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 and Fang [ChFa10] proved the stronger statement that if and are infinite sets such that contains all large integers and They later [ChFa14] improved to .
∀ (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 - √3) → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTopSolvedStatement only, no proof