Erdős Problem 28

Reference: erdosproblems.com/28

theorem 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$.