Documentation

FormalConjectures.ErdosProblems.«868»

Erdős Problem 868 #

References:

source
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
Instances For
    source
    theorem Erdos868.erdos_868.parts.i :
    False ↔ ∀ (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

    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$?

    Larsen and Larsen [LaLa26] answered this in the negative.

    source
    theorem Erdos868.erdos_868.parts.ii :
    False ↔ ∀ (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

    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$?

    Larsen and Larsen [LaLa26] constructed a counterexample with $f(n) > c \log n$ for all large $n$.

    source
    theorem Erdos868.erdos_868.variants.fixed_ε :
    True ↔ ∀ (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

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

    source
    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.