The density of the divisor sum set is asymptotically equivalent to $c_1 / \log(t)^{c_2}$.

1∃ c₁ > 0,2  ∃ c₂ > 0,3    ∃ d,4      (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧5        Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂