FormalConjectures/ErdosProblems/1049.lean

GitHub source file

5 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos1049.erdos_1049 Let $t>1$ be a rational number sorry line 43 source

   Source documentation

   Let $t>1$ be a rational number. Is $\sum_{n=1}^\infty\frac{1}{t^n-1}=\sum_{n=1}^\infty \frac{\tau(n)}{t^n}$ irrational, where $\tau(n)$ counts the divisors of $n$?

   A conjecture of Chowla.

   depends on sorry what this means

   Statement uses: Iff, True, Rat, GT.gt, OfNat.ofNat, Irrational, tsum, Real, PNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, SummationFilter.unconditional

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

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_1049 :
       answer(sorry) ↔ ∀ t : ℚ, t > 1 → Irrational (∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1)) := by
   …

2. theorem Erdos1049.erdos_1049.variants.geq_2_integer sorry line 52 source

   depends on sorry what this means

   Statement uses: Int, GE.ge, OfNat.ofNat, Irrational, tsum, Real, PNat, HDiv.hDiv, HSub.hSub, HPow.hPow, Nat, SummationFilter.unconditional

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

   41 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

3. lemma Erdos1049.lambert_convergent Convergent case (|t| > 1) line 66 source

   Source documentation

   Convergent case (|t| > 1).

   Substitute r := t⁻¹ so ‖r‖ < 1, then apply Mathlib's series identity tsum_pow_div_one_sub_eq_tsum_sigma at k = 0: $$\sum_{n \ge 1} \frac{r^n}{1 - r^n} = \sum_{n \ge 1} \sigma_0(n) \cdot r^n.$$ After clearing denominators, both sides match the Lambert identity: LHS becomes 1/(t^n - 1) and RHS becomes τ(n) / t^n.

   private lemma lambert_convergent (t : ℝ) (ht : 1 < |t|) :
       ∑' n : ℕ+, 1 / (t ^ (n : ℕ) - 1) =
       ∑' n : ℕ+, ((n : ℕ).divisors.card : ℝ) / (t ^ (n : ℕ)) := by
   …

4. lemma Erdos1049.lambert_divergent Divergent case (|t| ≤ 1) line 120 source

   Source documentation

   Divergent case (|t| ≤ 1).

   Both tsums equal 0 in this regime, but for different reasons in each sub-case. We split on t ∈ {1, 0, -1} and the generic |t| < 1, t ≠ 0 remainder, and use the same key non-summability lemma below to handle the cases where the series diverges.

   • t = 1: every LHS term is 1 / (1 - 1) = 0 (Lean convention), so the LHS sum is trivially 0. RHS is Σ τ(n), non-summable.
   • t = 0: every RHS term is τ(n) / 0 = 0 (Lean convention), so the RHS sum is trivially 0. LHS is Σ (-1), non-summable.
   • t = -1: alternating; LHS vanishes at even n but odd n give terms of magnitude 1/2, an infinite set. RHS terms have magnitude τ(n) ≥ 1.
   • |t| < 1, t ≠ 0: standard; bounded denominator gives lower-bounded reciprocal on LHS, and |t^n| ≤ 1 plus τ(n) ≥ 1 gives the RHS bound.

   In every case, Lean's tsum_eq_zero_of_not_summable collapses the non- summable side to 0, matching the 0 on the other side.

   private lemma lambert_divergent (t : ℝ) (ht : |t| ≤ 1) :
       ∑' n : ℕ+, 1 / (t ^ (n : ℕ) - 1) =
       ∑' n : ℕ+, ((n : ℕ).divisors.card : ℝ) / (t ^ (n : ℕ)) := by
   …

5. theorem Erdos1049.lambert_series_eq_num_divisor_sum The classical Lambert series identity: $\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}$, where $\tau(n)$ counts the divisors of $n$ line 249 source

   Source documentation

   The classical Lambert series identity: $\sum_{n=1}^\infty \frac{1}{t^n - 1} = \sum_{n=1}^\infty \frac{\tau(n)}{t^n}$, where $\tau(n)$ counts the divisors of $n$.

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

   Statement uses: Rat, Eq, Real, tsum, PNat, HDiv.hDiv, OfNat.ofNat, HSub.hSub, HPow.hPow, Nat, SummationFilter.unconditional, Finset.card, Nat.divisors

   Proof uses: LT.lt, abs, LE.le, Or, lt_or_ge

   50 instances, coercions and auxiliary constants left out.

   Tactic trace: 6 steps

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

   theorem lambert_series_eq_num_divisor_sum : ∀ t : ℚ,
        ∑' n : ℕ+, 1 / ((t : ℝ) ^ (n : ℕ) - 1) =
        ∑' n : ℕ+, (n : ℕ).divisors.card / ((t : ℝ) ^ (n : ℕ)) := by
   …