Erdős Problem 868

Reference: erdosproblems.com/868

noncomputable def Erdos868.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

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

theorem Erdos868.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 Erdos868.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 Erdos868.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 Erdos868.erdos_868.variants.Hartter_Nathanson (o : ℕ) (ho : 1 < o) : ∃ (A : Set ℕ), 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.