FormalConjectures/ErdosProblems/868.lean

GitHub source file

5 declarations, 4 contain sorry, 0 declared as axioms

1. def Erdos868.ncard_add_repr line 40 source

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Set, Nat

   Proof uses: Set.ncard, Fin, Set.ofPred, And, Monotone, LE.le, Set.range, Eq, Finset.sum, Finset.univ

   6 instances, coercions and auxiliary constants left out.

2. theorem Erdos868.erdos_868.parts.i 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$ sorry line 50 source

   Source documentation

   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.

   depends on sorry what this means

   Statement uses: Iff, False, Set, Nat, Set.IsAsymptoticAddBasisOfOrder, OfNat.ofNat, Filter.Tendsto, Erdos868.ncard_add_repr, Filter.atTop, Exists, And, LE.le, Membership.mem, Not, SDiff.sdiff, Singleton.singleton

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   14 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: Erdos868.ncard_add_repr

3. theorem Erdos868.erdos_868.parts.ii 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$ sorry line 64 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Iff, False, Set, Nat, Real, GT.gt, OfNat.ofNat, Set.IsAsymptoticAddBasisOfOrder, Filter.Eventually, LT.lt, HMul.hMul, Real.log, Erdos868.ncard_add_repr, Filter.atTop, Exists, And, LE.le, Membership.mem, Not, SDiff.sdiff and 1 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: Erdos868.ncard_add_repr

4. theorem Erdos868.erdos_868.variants.fixed_ε Erdős and Nathanson proved that this is true if $f(n) > c \log n$ for all large $n$, for some fixed constant $c > (\log \frac{4}{3})^{-1}$ sorry line 73 source

   Source documentation

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

   depends on sorry what this means

   Statement uses: Iff, True, Set, Nat, Real, GT.gt, Inv.inv, Real.log, HDiv.hDiv, OfNat.ofNat, Set.IsAsymptoticAddBasisOfOrder, Filter.Eventually, LT.lt, HMul.hMul, Erdos868.ncard_add_repr, Filter.atTop, Exists, And, LE.le, Membership.mem and 3 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

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

   Mentions: c, Erdos868.ncard_add_repr

5. theorem Erdos868.erdos_868.variants.Hartter_Nathanson sorry line 84 source

   depends on sorry what this means

   Statement uses: Nat, LT.lt, OfNat.ofNat, Exists, Set, And, Set.IsAsymptoticAddBasisOfOrder, LE.le, Membership.mem, SDiff.sdiff, Singleton.singleton

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   14 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.