Erdős problem 785
Let be infinite sets such that contains all large integers. Let and similarly for . Is it true that if then as ?
Sources
FormalConjectures/ErdosProblems/
785.lean
Retained formal statement
Chen conjectures that this should be true with .
True ↔ ∀ (A B : Set ℕ), A.Infinite → B.Infinite → IsAdditiveComplement A B → Filter.limsup (fun x => ↑(↑(Erdos785.counting A x) * ↑(Erdos785.counting B x)) / ↑↑x) Filter.atTop < ↑(3 / 2) → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTopOpenStatement only, no proof