From 87aeaf7a609030cac3ccc29164a7fb22392f6367 Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Fri, 10 Jul 2026 15:40:33 +0100 Subject: [PATCH 1/2] Add theorem `pow_eq_sum_stirlingSecond_mul_descFactorial` in `Stirling.lean` --- .../Combinatorics/Enumerative/Stirling.lean | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/Mathlib/Combinatorics/Enumerative/Stirling.lean b/Mathlib/Combinatorics/Enumerative/Stirling.lean index 251fbe7940ceb5..b1f7588cde3537 100644 --- a/Mathlib/Combinatorics/Enumerative/Stirling.lean +++ b/Mathlib/Combinatorics/Enumerative/Stirling.lean @@ -5,6 +5,7 @@ Authors: Beibei Xiong, Yu Shao, Weijie Jiang, Zhengfeng Yang -/ module +public import Mathlib.Algebra.BigOperators.Ring.Finset public import Mathlib.Data.Nat.Factorial.Basic public import Mathlib.Data.Nat.Choose.Basic public import Mathlib.Tactic.NormNum.Inv @@ -169,4 +170,26 @@ theorem stirlingSecond_succ_self_left (n : ℕ) : rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one, Nat.choose_succ_succ (n + 1), Nat.choose_one_right] +theorem descFactorial_mul_self (n j : ℕ) : + n.descFactorial j * n = n.descFactorial (j + 1) + j * n.descFactorial j := by + rcases le_or_gt j n with h | h <;> + grind [descFactorial_succ, add_mul, descFactorial_eq_zero_iff_lt] + +theorem pow_eq_sum_stirlingSecond_mul_descFactorial (n k : ℕ) : + n ^ k = ∑ j ∈ Finset.range (k + 1), stirlingSecond k j * n.descFactorial j := by + induction k with + | zero => simp + | succ k ih => + have : ∑ j ∈ Finset.range (k + 1), stirlingSecond k j * (j * n.descFactorial j) + = ∑ j ∈ Finset.range (k + 1), + (j + 1) * (stirlingSecond k (j + 1) * n.descFactorial (j + 1)) := by + grind [Finset.sum_range_succ' (fun j ↦ stirlingSecond k j * (j * n.descFactorial j)) k, + Finset.sum_range_succ (fun j ↦ (j + 1) * (stirlingSecond k (j + 1) * + n.descFactorial (j + 1))) k, stirlingSecond_eq_zero_of_lt k.lt_add_one] + rw [pow_succ, ih, Finset.sum_mul, + Finset.sum_range_succ' (fun j ↦ stirlingSecond (k + 1) j * n.descFactorial j) (k + 1)] + simp only [mul_assoc, descFactorial_mul_self, mul_add, Finset.sum_add_distrib, this, + stirlingSecond_succ_succ, add_mul, stirlingSecond_succ_zero, zero_mul, add_zero] + grind + end Nat From 517f05b92d6701464e6b4606e87bfb3c8f5f62cd Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Fri, 10 Jul 2026 15:44:15 +0100 Subject: [PATCH 2/2] Generalize the sum to `(n : R) ^ k * x ^ n` from `(n : R) ^ 2 * x ^ n` --- Mathlib/Analysis/SpecificLimits/Normed.lean | 111 +++++++++++++------- 1 file changed, 72 insertions(+), 39 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index c90f31934ccdc9..c562e5a11e1c9c 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -13,6 +13,7 @@ public import Mathlib.Analysis.Normed.Ring.InfiniteSum public import Mathlib.Analysis.Normed.Module.Basic public import Mathlib.Analysis.Normed.Order.Lattice public import Mathlib.Analysis.SpecificLimits.Basic +public import Mathlib.Combinatorics.Enumerative.Stirling public import Mathlib.Data.List.TFAE public import Mathlib.Data.Nat.Choose.Bounds public import Mathlib.Data.Nat.Choose.Cast @@ -549,47 +550,79 @@ theorem tsum_coe_mul_geometric_of_norm_lt_one {r : 𝕜} (hr : ‖r‖ < 1) : (∑' n : ℕ, n * r ^ n : 𝕜) = r / (1 - r) ^ 2 := (hasSum_coe_mul_geometric_of_norm_lt_one hr).tsum_eq -/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3`, `HasSum` version in -a general ring with summable geometric series. For a version in a field, using division instead -of `Ring.inverse`, see `hasSum_sq_mul_geometric_of_norm_lt_one`. -/ -theorem hasSum_sq_mul_geometric_of_norm_lt_one' {x : R} (h : ‖x‖ < 1) : - HasSum (fun n : ℕ ↦ (n : R) ^ 2 * x ^ n) (x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3) := by - have A : HasSum (fun n : ℕ ↦ ((n + 2).choose 2 : R) * x ^ n) ((1 - x)⁻¹ʳ ^ 3) := - hasSum_choose_mul_geometric_of_norm_lt_one' 2 h - have B : HasSum (fun (n : ℕ) ↦ (n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2) := by - convert! hasSum_choose_mul_geometric_of_norm_lt_one' 1 h with n - simp - have C : HasSum (fun n ↦ n * x ^ n : ℕ → R) (x * (1 - x)⁻¹ʳ ^ 2) := - hasSum_coe_mul_geometric_of_norm_lt_one' h - convert! ((A.mul_left 2).sub (B.mul_left 2)).sub C using 1 - · ext n - rw [← mul_assoc, Nat.two_mul_cast_choose_two, pow_two, cast_add, cast_ofNat] - noncomm_ring - · symm - calc 2 * (1 - x)⁻¹ʳ ^ 3 - 2 * (1 - x)⁻¹ʳ ^ 2 - x * (1 - x)⁻¹ʳ ^ 2 - _ = 2 * (1 - x)⁻¹ʳ ^ 3 - 2 * (((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ ^ 2) - - x * (((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ ^ 2) := by - simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)] - _ = x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3 := by noncomm_ring - -/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3`, version in a general -ring with summable geometric series. For a version in a field, using division instead of -`Ring.inverse`, see `tsum_sq_mul_geometric_of_norm_lt_one`. -/ -theorem tsum_sq_mul_geometric_of_norm_lt_one' {x : R} (h : ‖x‖ < 1) : - ∑' n : ℕ, (n : R) ^ 2 * x ^ n = x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3 := - (hasSum_sq_mul_geometric_of_norm_lt_one' h).tsum_eq - -/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3`, -`HasSum` version. -/ -theorem hasSum_sq_mul_geometric_of_norm_lt_one {r : 𝕜} (hr : ‖r‖ < 1) : - HasSum (fun n : ℕ ↦ (n : 𝕜) ^ 2 * r ^ n) (r * (1 + r) / (1 - r) ^ 3) := by - convert! hasSum_sq_mul_geometric_of_norm_lt_one' hr using 1 +theorem hasSum_descFactorial_mul_geometric_of_norm_lt_one' (j : ℕ) {x : R} (h : ‖x‖ < 1) : + HasSum (fun n : ℕ ↦ (n.descFactorial j : R) * x ^ n) + ((j.factorial : R) * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) := by + have hx : Commute (x ^ j) (((1 - x)⁻¹ʳ) ^ (j + 1)) := by + obtain ⟨u, hu⟩ := isUnit_one_sub_of_norm_lt_one h + have hxu : Commute x (u : R) := hu.symm ▸ (Commute.one_right x).sub_right (Commute.refl x) + simp [← hu, hxu.units_inv_right.pow_pow] + have A := ((hasSum_choose_mul_geometric_of_norm_lt_one' j h).mul_left + (j.factorial : R)).mul_right (x ^ j) + have Afun : (fun m : ℕ ↦ (j.factorial : R) * (((m + j).choose j : R) * x ^ m) * x ^ j) + = fun m : ℕ ↦ ((m + j).descFactorial j : R) * x ^ (m + j) := by + funext m + push_cast [Nat.descFactorial_eq_factorial_mul_choose] + simp only [pow_add, mul_assoc] + rw [Afun] at A + have B := (hasSum_nat_add_iff (f := fun n : ℕ ↦ (n.descFactorial j : R) * x ^ n) j).mp A + have hzero : ∑ i ∈ Finset.range j, (i.descFactorial j : R) * x ^ i = 0 := + Finset.sum_eq_zero fun i hi ↦ by + simp [descFactorial_eq_zero_iff_lt.2 (Finset.mem_range.1 hi)] + simpa only [hzero, add_zero, mul_assoc, hx.symm.eq] using B + +/-- If `‖x‖ < 1`, then `∑' n : ℕ, n ^ k * x ^ n` is given by the finite sum +`∑ j ∈ range (k + 1), S(k, j) * j ! * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)`, +where `S(k, j)` denotes the Stirling numbers of the second kind. -/ +theorem hasSum_pow_mul_geometric_of_norm_lt_one' (k : ℕ) {x : R} (h : ‖x‖ < 1) : + HasSum (fun n : ℕ ↦ (n : R) ^ k * x ^ n) + (∑ j ∈ Finset.range (k + 1), + (stirlingSecond k j : R) * j.factorial * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) := by + have hfun : (fun n : ℕ ↦ (n : R) ^ k * x ^ n) = fun n : ℕ ↦ ∑ j ∈ Finset.range (k + 1), + (stirlingSecond k j : R) * ((n.descFactorial j : R) * x ^ n) := by + funext n + rw [← Nat.cast_pow, Nat.pow_eq_sum_stirlingSecond_mul_descFactorial n k, Nat.cast_sum, + Finset.sum_mul] + simp only [Nat.cast_mul, mul_assoc] + have hval : (∑ j ∈ Finset.range (k + 1), + (stirlingSecond k j : R) * j.factorial * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) + = ∑ j ∈ Finset.range (k + 1), (stirlingSecond k j : R) + * ((j.factorial : R) * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) := by + simp only [mul_assoc] + rw [hfun, hval] + exact hasSum_sum fun j _ ↦ + (hasSum_descFactorial_mul_geometric_of_norm_lt_one' j h).mul_left _ + +theorem tsum_pow_mul_geometric_of_norm_lt_one' (k : ℕ) {x : R} (h : ‖x‖ < 1) : + ∑' n : ℕ, (n : R) ^ k * x ^ n = (∑ j ∈ Finset.range (k + 1), + (stirlingSecond k j : R) * j.factorial * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) := + (hasSum_pow_mul_geometric_of_norm_lt_one' k h).tsum_eq + +theorem hasSum_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : + HasSum (fun n : ℕ ↦ (n : 𝕜) ^ k * r ^ n) + (∑ j ∈ Finset.range (k + 1), + stirlingSecond k j * j.factorial * r ^ j / (1 - r) ^ (j + 1)) := by + convert! hasSum_pow_mul_geometric_of_norm_lt_one' k hr using 1 simp [div_eq_mul_inv] -/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3`. -/ -theorem tsum_sq_mul_geometric_of_norm_lt_one {r : 𝕜} (hr : ‖r‖ < 1) : - ∑' n : ℕ, (n : 𝕜) ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3 := - (hasSum_sq_mul_geometric_of_norm_lt_one hr).tsum_eq +theorem tsum_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : + ∑' n : ℕ, (n : 𝕜) ^ k * r ^ n = (∑ j ∈ Finset.range (k + 1), + stirlingSecond k j * j.factorial * r ^ j / (1 - r) ^ (j + 1)) := + (hasSum_pow_mul_geometric_of_norm_lt_one k hr).tsum_eq + +theorem hasSum_sq_mul_geometric_of_norm_lt_one' {x : R} (h : ‖x‖ < 1) : + HasSum (fun n : ℕ ↦ (n : R) ^ 2 * x ^ n) (x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3) := by + have h1 : (∑ j ∈ Finset.range (2 + 1), + (stirlingSecond 2 j : R) * j.factorial * x ^ j * ((1 - x)⁻¹ʳ) ^ (j + 1)) + = x * ((1 - x)⁻¹ʳ) ^ 2 + 2 * (x ^ 2 * ((1 - x)⁻¹ʳ) ^ 3) := by + simp [Finset.sum_range_succ, stirlingSecond, Nat.factorial, mul_assoc] + have h2 : x * ((1 - x)⁻¹ʳ) ^ 2 + 2 * (x ^ 2 * ((1 - x)⁻¹ʳ) ^ 3) + = x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3 := by + calc x * ((1 - x)⁻¹ʳ) ^ 2 + 2 * (x ^ 2 * ((1 - x)⁻¹ʳ) ^ 3) + = x * (((1 - x) * (1 - x)⁻¹ʳ) * ((1 - x)⁻¹ʳ) ^ 2) + 2 * (x ^ 2 * ((1 - x)⁻¹ʳ) ^ 3) := by + grind [Ring.mul_inverse_cancel, isUnit_one_sub_of_norm_lt_one] + _ = x * (1 + x) * ((1 - x)⁻¹ʳ) ^ 3 := by grind + grind [hasSum_pow_mul_geometric_of_norm_lt_one'] end MulGeometric