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 : IsLeast {c : EReal | ∃ (A : Set ℕ), AdditiveBasisCondition A ∧ ↑(Filter.limsup (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / √↑N) Filter.atTop) = c} 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) = 0 sup n → ∞ |A ∩ {1, …, N}| / N^(1/2) = 0?

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

Erdos observed that this value is finite and > 1.

theorem Erdos33.erdos_33.variants.vanDoorn : ↑(2 * goldenRatio ^ (5 / 2)) ∈ lowerBounds {c : EReal | ∃ (A : Set ℕ), AdditiveBasisCondition A ∧ ↑(Filter.limsup (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / √↑N) Filter.atTop) = c}

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