FormalConjectures/ErdosProblems/124.lean

GitHub source file

6 declarations, 5 contain sorry, 0 declared as axioms

1. def Erdos124.sumsOfDistinctPowers The set of integers which are the sum of distinct powers d ^ i with i ≥ k line 36 source

   Source documentation

   The set of integers which are the sum of distinct powers d ^ i with i ≥ k.

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

   Statement uses: Nat, Set

   Proof uses: Set.ofPred, Exists, Finset, And, Membership.mem, LE.le, Eq, Finset.sum, HPow.hPow

   8 instances, coercions and auxiliary constants left out.

   def sumsOfDistinctPowers (d k : ℕ) : Set ℕ :=
   …

2. lemma Erdos124.erdos124.zero Documented declaration: zero sorry line 48 source

   Source documentation

   Let $3 \le d_1 < d_2 < \dots < d_r$ be integers such that $$\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.$$ Can all sufficiently large integers be written as a sum of the shape $\sum_i c_ia_i$ where $c_i \in \{0, 1\}$ and $a_i$ has only the digits $0, 1$ when written in base $d_i$?

   Conjectured by Erdős [Er97], solved by Boris Alexeev using Aristotle.

   depends on sorry what this means

   Statement uses: Iff, True, Finset, Nat, Membership.mem, LE.le, OfNat.ofNat, Rat, Finset.sum, Inv.inv, HSub.hSub, Filter.Eventually, Set, Erdos124.sumsOfDistinctPowers, Filter.atTop

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

   32 instances, coercions and auxiliary constants left out.

   lemma erdos124.zero : answer(True) ↔
       ∀ D : Finset ℕ, (∀ d ∈ D, 3 ≤ d) → 1 ≤ ∑ d ∈ D, (d - 1 : ℚ)⁻¹ →
         ∀ᶠ n in atTop, n ∈ ∑ d ∈ D, sumsOfDistinctPowers d 0 := sorry
   …

   Mentions: Erdos124.sumsOfDistinctPowers

3. lemma Erdos124.erdos124.ne_zero Documented declaration: ne_zero sorry line 62 source

   Source documentation

   Let $k \ne 0$ and $3\leq d_1 < d_2 < \cdots < d_r$ be integers of gcd equal to $1$ such that $$\sum_{1 \le i \le r}\frac 1{d_i - 1} \ge 1.$$ Can all sufficiently large integers be written as a sum of the shape $\sum_i c_ia_i$ where $c_i \in \{0, 1\}$ and $a_i$ is divisible by $d_i ^ k$ and has only the digits $0, 1$ when written in base $d_i$?

   Conjectured by Burr, Erdős, Graham, and Li [BEGL96]

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Ne, OfNat.ofNat, Finset, Membership.mem, LE.le, Rat, Finset.sum, Inv.inv, HSub.hSub, Eq, Finset.gcd, id, Filter.Eventually, Set, Erdos124.sumsOfDistinctPowers, Filter.atTop

   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.

   lemma erdos124.ne_zero : answer(sorry) ↔
       ∀ k ≠ 0, ∀ D : Finset ℕ, (∀ d ∈ D, 3 ≤ d) → 1 ≤ ∑ d ∈ D, (d - 1 : ℚ)⁻¹ → D.gcd id = 1 →
         ∀ᶠ n in atTop, n ∈ ∑ d ∈ D, sumsOfDistinctPowers d k := by
   …

   Mentions: Erdos124.sumsOfDistinctPowers

4. lemma Erdos124.erdos124.ne_zero_three_four_seven Documented declaration: ne_zero_three_four_seven sorry line 75 source

   Source documentation

   All sufficiently large integers can be written as $a + b + c$, where $a$, $b$, and $c$ are divisible by $3$, $4$, and $7$ respectively, and after division by that base have only the digits $0, 1$ in that base.

   Proved by Burr, Erdős, Graham, and Li [BEGL96]

   depends on sorry what this means

   Statement uses: Filter.Eventually, Nat, Membership.mem, Set, HAdd.hAdd, Erdos124.sumsOfDistinctPowers, OfNat.ofNat, Filter.atTop

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

   12 instances, coercions and auxiliary constants left out.

   lemma erdos124.ne_zero_three_four_seven :
       ∀ᶠ n in atTop,
         n ∈ sumsOfDistinctPowers 3 1 + sumsOfDistinctPowers 4 1 + sumsOfDistinctPowers 7 1 :=
   …

   Mentions: Erdos124.sumsOfDistinctPowers

5. lemma Erdos124.erdos124.converse sorry line 90 source

   depends on sorry what this means

   Statement uses: Finset, Nat, Membership.mem, LE.le, OfNat.ofNat, Filter.Eventually, Set, Finset.sum, Erdos124.sumsOfDistinctPowers, Filter.atTop, Rat, Inv.inv, HSub.hSub

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

   32 instances, coercions and auxiliary constants left out.

6. lemma Erdos124.erdos124.melfi_construction Documented declaration: melfi_construction sorry line 107 source

   Source documentation

   For any $\varepsilon > 0$, there exists an infinite sequence $2 \le d_0 < d_1 < \dots$ such that the series $\sum_{i=0}^{\infty} \frac{1}{d_i - 1}$ converges to a value at most $\varepsilon$, and yet for every $k \ne 0$ all sufficiently large integers can be written as $\sum_{i \in I} a_i$ for some finite set $I$, where each $a_i$ is divisible by $d_i^k$ and has only the digits $0, 1$ when written in base $d_i$.

   The restriction $k \ne 0$ excludes the degenerate representation of $n$ as a sum of $n$ copies of $1 = d_i^0$ taken from $n$ distinct bases.

   Proved by Melfi [Me04, Proposition 1]

   depends on sorry what this means

   Statement uses: Real, LT.lt, OfNat.ofNat, Exists, Nat, And, StrictMono, LE.le, Summable, Inv.inv, HSub.hSub, SummationFilter.unconditional, tsum, Ne, Filter.Eventually, Finset, Membership.mem, Set, Erdos124.sumsOfDistinctPowers, Eq and 2 more

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

   44 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   lemma erdos124.melfi_construction {ε : ℝ} (hε : 0 < ε) :
       ∃ d : ℕ → ℕ, StrictMono d ∧ 2 ≤ d 0 ∧
         Summable (fun i ↦ (d i - 1 : ℝ)⁻¹) ∧ ∑' i, (d i - 1 : ℝ)⁻¹ ≤ ε ∧ ∀ k ≠ 0, ∀ᶠ n in atTop,
         ∃ (I : Finset ℕ) (a : ℕ → ℕ), (∀ i ∈ I, a i ∈ sumsOfDistinctPowers (d i) k) ∧
           ∑ i ∈ I, a i = n := by
   …

   Mentions: Erdos124.sumsOfDistinctPowers