Erdős problem 868
Let be an additive basis of order , let denote the number of ways in which can be written as the sum of two elements from . If for large and an arbitrary fixed , then must contain a minimal additive basis of order ?
Sources
FormalConjectures/ErdosProblems/
868.lean
Retained formal statement
Let be an additive basis of order , let denote the number of ways in which can be written as the sum of two elements from . If for large and an arbitrary fixed , then must contain a minimal additive basis of order ?
Larsen and Larsen [LaLa26] constructed a counterexample with for all large .
False ↔ ∀ (A : Set ℕ), ∀ ε > 0, A.IsAsymptoticAddBasisOfOrder 2 → (∀ᶠ (n : ℕ) in Filter.atTop, ε * Real.log ↑n < ↑(Erdos868.ncard_add_repr A 2 n)) → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2SolvedStatement only, no proof