Erdős Problem 868

Reference: erdosproblems.com/868

noncomputable def ncard_add_repr (A : Set ℕ) (o n : ℕ) : ℕ

The number of ways in which a natural n can be written as the sum of o members of the set A.

Equations

• ncard_add_repr A o n = {a : Fin o → ℕ | Set.range a ⊆ A ∧ ∑ i : Fin o, a i = n}.ncard

theorem erdos_868.parts.i : (∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → Filter.Tendsto (fun (n : ℕ) => ncard_add_repr A 2 n) Filter.atTop Filter.atTop → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2) ↔ sorry

Let $A$ be an additive basis of order $2$, let $f(n)$ denote the number of ways in which $n$ can be written as the sum of two elements from $A$. If $f(n)\to\infty$ as $n\to\infty$, then must $A$ contain a minimal additive basis of order $2$?

theorem erdos_868.parts.ii : (∀ (A : Set ℕ), ∀ ε > 0, A.IsAsymptoticAddBasisOfOrder 2 → (∀ᶠ (n : ℕ) in Filter.atTop, ε * Real.log ↑n < ↑(ncard_add_repr A 2 n)) → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2) ↔ sorry

Let $A$ be an additive basis of order $2$, let $f(n)$ denote the number of ways in which $n$ can be written as the sum of two elements from $A$. If $f(n)>\epsilon\log n$ for large $n$ and an arbitrary fixed $\epsilon > 0$, then must $A$ contain a minimal additive basis of order $2$?

theorem erdos_868.variants.fixed_ε : (∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → (∀ᶠ (n : ℕ) in Filter.atTop, (Real.log (4 / 3))⁻¹ * Real.log ↑n < ↑(ncard_add_repr A 2 n)) → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2) ↔ True

Erdős and Nathanson proved that this is true if $f(n) > (\log\frac{4}{3})^{-1}\log n$ for all large $n$.

theorem erdos_868.variants.Hartter_Nathanson : ∃ (A : Set ℕ), ∃ o > 1, A.IsAsymptoticAddBasisOfOrder o ∧ ∀ B ⊆ A, B.IsAsymptoticAddBasisOfOrder o → ∃ b ∈ B, (B \ {b}).IsAsymptoticAddBasisOfOrder o

Härtter and Nathanson proved that there exist additive bases which do not contain any minimal additive bases.