Erdős problem 859

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

859.lean

Retained formal statement4 of 4

A case where we can easily calculate the density of DivisorSumSet t is that of t=0.

FormalConjectures/ErdosProblems/859.leanErdos859.erdos_859.variants.trivial_case1 lineExact file

1Erdos859.DivisorSumSet 0 = Set.univ

TextbookStatement only, no proof