Erdős problem 28

If $A ⊆ \mathbb{N}$ is such that $A + A$ contains all but finitely many integers then $\limsup 1_A ∗ 1_A(n) = \infty$ .

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

28.lean

Retained formal statement1 of 1

If $A ⊆ \mathbb{N}$ is such that $A + A$ contains all but finitely many integers then $\limsup 1_A ∗ 1_A(n) = \infty$ .

FormalConjectures/ErdosProblems/28.leanErdos28.erdos_281 lineExact file

1∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

OpenStatement only, no proof