Skip to content

Erdős problem 868

Start work

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

868.lean

Retained formal statement3 of 4

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

FormalConjectures/ErdosProblems/868.leanErdos868.erdos_868.variants.fixed_ε5 linesExact file
True ↔  ∀ (A : Set ℕ),    A.IsAsymptoticAddBasisOfOrder 2 →      (∀ᶠ (n : ℕ) in Filter.atTop, (Real.log (4 / 3))⁻¹ * Real.log ↑n < ↑(Erdos868.ncard_add_repr A 2 n)) →        ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2
SolvedStatement only, no proof