Erdős problem 692
Let be the density of the set of integers with exactly one divisor in . Is unimodular for (i.e. increases until some then decreases thereafter)?
Sources
FormalConjectures/ErdosProblems/
692.lean
Retained formal statement
Erdős proved that for all , for some constant .
∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∃ c > 0, ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ), δ n m ≤ C / Real.log ↑n ^ cSolvedStatement only, no proof