Erdős problem 749
Let . Does there exist such that the lower density of is at least and yet for all ?
Sources
FormalConjectures/ErdosProblems/
749.lean
Retained formal statement
Let . Does there exist such that the lower density of is at least and yet for all ?
True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1OpenStatement only, no proof