Erdős problem 12
Let be infinite with no distinct such that with . Can have positive lower limit? Must every such fall below infinitely often?
Sources
FormalConjectures/ErdosProblems/
12.lean
Retained formal statement
Given any function as there exists a set with the property that there are no distinct such that and , such that there are infinitely many such that $$\lvert A\cap\{1,\ldots,N\}\rvert > \frac{N}{f(N)}.
∀ (f : ℕ → ℕ), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ A, Erdos12.IsGood A ∧ {N | ↑N / ↑(f N) < ↑(A ∩ Set.Icc 1 N).ncard}.InfiniteSolvedStatement only, no proof