Erdős Problem 33

Reference: erdosproblems.com/33

def Erdos33.AdditiveBasisCondition (A : Set ℕ) : Prop

Let A ⊆ ℕ be a set such that every integer can be written as n^2 + a for some a in A and n ≥ 0.

Equations

• Erdos33.AdditiveBasisCondition A = ∀ (k : ℕ), ∃ (n : ℕ), ∃ a ∈ A, k = a + n ^ 2

theorem Erdos33.erdos_33 : ⨅ (A : ↑{A : Set ℕ | AdditiveBasisCondition A}), Filter.limsup (fun (N : ℕ) => ↑(↑A ∩ Set.Icc 1 N).ncard / ↑√↑N) Filter.atTop = sorry

Let A ⊆ ℕ be a set such that every integer can be written as n^2 + a for some a in A and n ≥ 0. What is the smallest possible value of lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) sup n → ∞ |A ∩ {1, …, N}| / N^(1/2)?

theorem Erdos33.erdos_33.variants.one_mem_lowerBounds : ∃ (A : Set ℕ), AdditiveBasisCondition A ∧ 1 < Filter.limsup (fun (N : ℕ) => ↑(A ∩ Set.Icc 1 N).ncard / √↑N) Filter.atTop

Erdos observed that this value is finite and > 1.

theorem Erdos33.erdos_33.variants.vanDoorn : ⨅ (A : ↑{A : Set ℕ | AdditiveBasisCondition A}), Filter.limsup (fun (N : ℕ) => ↑(↑A ∩ Set.Icc 1 N).ncard / ↑√↑N) Filter.atTop ≤ ↑(2 * Real.goldenRatio ^ (5 / 2))

The smallest possible value of lim sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) is at most 2φ^(5/2) ≈ 6.66, with φ equal to the golden ratio. Proven by Wouter van Doorn.