Erdős Problem 28

Reference: erdosproblems.com/28

theorem Erdos28.erdos_28 (A : Set ℕ) (h : (A + A)ᶜ.Finite) : Filter.limsup (fun (n : ℕ) => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤

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