Skip to content

Erdős problem 859

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

859.lean

Retained formal statement2 of 4

A weaker version of the problem proved by Erdos: The density dₜ of DivisorSumSet (t : ℕ) is bounded from below by 1 / log (t) ^ c₃ and from above by 1 / log (t) ^ c₄ for some positive constants c₃ and c₄.

FormalConjectures/ErdosProblems/859.leanErdos859.erdos_859.variants.erdos_upper_lower_bounds5 linesExact file
∃ c₃ > 0,  ∃ c₄ > 0,    ∃ t₀,      ∀ᶠ (t : ℕ) in Filter.atTop,        ∃ dₜ, (Erdos859.DivisorSumSet t).HasDensity dₜ ∧ 1 / Real.log ↑t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log ↑t ^ c₄
SolvedStatement only, no proof