Erdős problem 245
Let be an infinite set such that . Is it true that
Sources
FormalConjectures/ErdosProblems/
245.lean
Retained formal statement
Let be an infinite set such that . Then
∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 2 ≤ Filter.limsup (fun N => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTopSolvedStatement only, no proof