Erdős Problem 41

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 : ℝ | ∃ (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 : 1 ∈ lowerBounds {c : ℝ | ∃ (A : Set ℕ), AdditiveBasisCondition A ∧ Filter.limsup (fun (N : ℕ) => ↑(A.interIcc 1 N).ncard / √↑N) Filter.atTop = c}

Erdos observed that this value is finite and > 1.

theorem Erdos33.erdos_33.variants.vanDoorn : 2 * goldenRatio ^ (5 / 2) ∈ lowerBounds {c : ℝ | ∃ (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.