Erdős Problem 859

Reference: erdosproblems.com/859

def Erdos859.DivisorSumSet (t : ℕ) : Set ℕ

DivisorSumSet t is the set of natural numbers n such that t can be represented as a sum of distinct divisors of n.

Equations

• Erdos859.DivisorSumSet t = {n : ℕ | ∃ s ⊆ n.divisors, t = ∑ i ∈ s, i}

theorem Erdos859.erdos_859.variants.erdos_upper_lower_bounds : ∃ c₃ > 0, ∃ c₄ > 0, ∃ (t₀ : ℕ), ∀ᶠ (t : ℕ) in Filter.atTop, ∃ (dₜ : ℝ), (DivisorSumSet t).HasDensity dₜ ∧ 1 / Real.log ↑t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log ↑t ^ c₄

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₄.

theorem Erdos859.erdos_859 : ∃ c₁ > 0, ∃ c₂ > 0, ∃ (d : ℕ → ℝ), (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun (t : ℕ) => d t) fun (t : ℕ) => c₁ / Real.log ↑t ^ c₂

theorem Erdos859.erdos_859.variants.trivial_case : DivisorSumSet 0 = Set.univ

theorem Erdos859.erdos_859.variants.positive_density (t : ℕ) : (DivisorSumSet t).HasPosDensity