Erdős problem 859 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

859.lean

Retained formal statement1 of 4

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

FormalConjectures/ErdosProblems/859.leanErdos859.erdos_8595 linesExact file

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₂

OpenStatement only, no proof

Sources

Search problems.science