feat(Analysis/SpecificLimits/Normed): the sum ∑' n, n ^ k * r ^ n via Stirling numbers

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -13,10 +13,9 @@ 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.Data.List.TFAE
+public import Mathlib.Combinatorics.Enumerative.Stirling
 public import Mathlib.Data.Nat.Choose.Bounds
 public import Mathlib.Order.Filter.AtTopBot.ModEq
-public import Mathlib.RingTheory.Polynomial.Pochhammer
 public import Mathlib.Tactic.NoncommRing
 
 /-!
@@ -478,57 +477,103 @@ lemma tsum_choose_mul_geometric_of_norm_lt_one (k : ℕ) {r : 𝕜} (hr : ‖r
     ∑' n, (n + k).choose k * r ^ n = 1 / (1 - r) ^ (k + 1) :=
   (hasSum_choose_mul_geometric_of_norm_lt_one k hr).tsum_eq
 
-lemma summable_descFactorial_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
-    Summable (fun n ↦ (n + k).descFactorial k * r ^ n) := by
-  convert! (summable_choose_mul_geometric_of_norm_lt_one k hr).mul_left (k.factorial : R) using
-    2 with n
-  simp [← mul_assoc, descFactorial_eq_factorial_mul_choose (n + k) k]
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n.descFactorial j * r ^ n = j ! * r ^ j / (1 - r) ^ (j + 1)`,
+`HasSum` version in a general ring with summable geometric series. For a version in a field,
+using division instead of `Ring.inverse`, see
+`hasSum_descFactorial_mul_geometric_of_norm_lt_one`. -/
+theorem hasSum_descFactorial_mul_geometric_of_norm_lt_one' (j : ℕ) {r : R} (h : ‖r‖ < 1) :
+    HasSum (fun n : ℕ ↦ (n.descFactorial j : R) * r ^ n)
+      ((j.factorial : R) * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1)) := by
+  rw [← hasSum_nat_add_iff' j]
+  convert! (hasSum_choose_mul_geometric_of_norm_lt_one' j h).mul_left
+    ((j.factorial : R) * r ^ j) using 1
+  · funext n
+    symm
+    push_cast [Nat.descFactorial_eq_factorial_mul_choose]
+    rw [mul_assoc, ((Nat.cast_commute ((n + j).choose j) (r ^ j)).symm).left_comm, ← pow_add,
+      add_comm j n, mul_assoc]
+  · exact sub_eq_self.2 <| Finset.sum_eq_zero fun i hi ↦ by
+      simp [descFactorial_eq_zero_iff_lt.2 (Finset.mem_range.1 hi)]
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n.descFactorial j * r ^ n = j ! * r ^ j / (1 - r) ^ (j + 1)`,
+version in a general ring with summable geometric series. For a version in a field, using
+division instead of `Ring.inverse`, see `tsum_descFactorial_mul_geometric_of_norm_lt_one`. -/
+theorem tsum_descFactorial_mul_geometric_of_norm_lt_one' (j : ℕ) {r : R} (h : ‖r‖ < 1) :
+    ∑' n : ℕ, (n.descFactorial j : R) * r ^ n
+      = (j.factorial : R) * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1) :=
+  (hasSum_descFactorial_mul_geometric_of_norm_lt_one' j h).tsum_eq
+
+lemma summable_descFactorial_mul_geometric_of_norm_lt_one (j : ℕ) {r : R} (hr : ‖r‖ < 1) :
+    Summable (fun n : ℕ ↦ (n.descFactorial j : R) * r ^ n) :=
+  (hasSum_descFactorial_mul_geometric_of_norm_lt_one' j hr).summable
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n.descFactorial j * r ^ n = j ! * r ^ j / (1 - r) ^ (j + 1)`,
+`HasSum` version. -/
+theorem hasSum_descFactorial_mul_geometric_of_norm_lt_one (j : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    HasSum (fun n : ℕ ↦ (n.descFactorial j : 𝕜) * r ^ n)
+      (j.factorial * r ^ j / (1 - r) ^ (j + 1)) := by
+  convert! hasSum_descFactorial_mul_geometric_of_norm_lt_one' j hr using 1
+  simp [div_eq_mul_inv]
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n.descFactorial j * r ^ n = j ! * r ^ j / (1 - r) ^ (j + 1)`. -/
+theorem tsum_descFactorial_mul_geometric_of_norm_lt_one (j : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    ∑' n : ℕ, (n.descFactorial j : 𝕜) * r ^ n = j.factorial * r ^ j / (1 - r) ^ (j + 1) :=
+  (hasSum_descFactorial_mul_geometric_of_norm_lt_one j hr).tsum_eq
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ k * r ^ n` is given by the finite sum
+`∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1)`, where `S(k, j)` denotes the
+Stirling numbers of the second kind. `HasSum` version in a general ring with summable geometric
+series. For a version in a field, using division instead of `Ring.inverse`, see
+`hasSum_pow_mul_geometric_of_norm_lt_one`. -/
+theorem hasSum_pow_mul_geometric_of_norm_lt_one' (k : ℕ) {r : R} (h : ‖r‖ < 1) :
+    HasSum (fun n : ℕ ↦ (n : R) ^ k * r ^ n)
+      (∑ j ∈ Finset.range (k + 1),
+        (stirlingSecond k j : R) * j.factorial * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1)) := by
+  simpa only [← Nat.cast_pow, Nat.pow_eq_sum_stirlingSecond_mul_descFactorial, Nat.cast_sum,
+    Nat.cast_mul, Finset.sum_mul, mul_assoc] using
+    hasSum_sum fun j _ ↦ (hasSum_descFactorial_mul_geometric_of_norm_lt_one' j h).mul_left _
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ k * r ^ n` is given by the finite sum
+`∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1)`, where `S(k, j)` denotes the
+Stirling numbers of the second kind. Version in a general ring with summable geometric series.
+For a version in a field, using division instead of `Ring.inverse`, see
+`tsum_pow_mul_geometric_of_norm_lt_one`. -/
+theorem tsum_pow_mul_geometric_of_norm_lt_one' (k : ℕ) {r : R} (h : ‖r‖ < 1) :
+    ∑' n : ℕ, (n : R) ^ k * r ^ n = (∑ j ∈ Finset.range (k + 1),
+      (stirlingSecond k j : R) * j.factorial * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1)) :=
+  (hasSum_pow_mul_geometric_of_norm_lt_one' k h).tsum_eq
 
-open Polynomial in
 theorem summable_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
-    Summable (fun n ↦ (n : R) ^ k * r ^ n : ℕ → R) := by
-  refine Nat.strong_induction_on k fun k hk => ?_
-  obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k
-      = n ^ k + ∑ i ∈ range k, a i * n ^ i := by
-    let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1)
-    refine ⟨fun i ↦ P.coeff i, fun n ↦ ?_⟩
-    have mP : Monic P := Monic.comp_X_add_C (monic_ascPochhammer ℕ k) _
-    have dP : P.natDegree = k := by
-      simp only [P, natDegree_comp, ascPochhammer_natDegree, mul_one, natDegree_X_add_C]
-    have A : (n + k).descFactorial k = P.eval n := by
-      have : n + 1 + k - 1 = n + k := by lia
-      simp [P, ascPochhammer_nat_eq_descFactorial, this]
-    conv_lhs => rw [A, mP.as_sum, dP]
-    simp [eval_finsetSum]
-  have : Summable (fun n ↦ (n + k).descFactorial k * r ^ n
-      - ∑ i ∈ range k, a i * n ^ (i : ℕ) * r ^ n) := by
-    apply (summable_descFactorial_mul_geometric_of_norm_lt_one k hr).sub
-    apply summable_sum (fun i hi ↦ ?_)
-    simp_rw [mul_assoc]
-    simp only [Finset.mem_range] at hi
-    exact (hk _ hi).mul_left _
-  convert! this using 1
-  ext n
-  simp [ha n, add_mul, sum_mul]
+    Summable (fun n ↦ (n : R) ^ k * r ^ n : ℕ → R) :=
+  (hasSum_pow_mul_geometric_of_norm_lt_one' k hr).summable
+
+/-- If `‖r‖ < 1`, then `∑' n : ℕ, n ^ k * r ^ n` is given by the finite sum
+`∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j / (1 - r) ^ (j + 1)`, where `S(k, j)` denotes the
+Stirling numbers of the second kind. `HasSum` version. -/
+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 ^ k * r ^ n` is given by the finite sum
+`∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j / (1 - r) ^ (j + 1)`, where `S(k, j)` denotes the
+Stirling numbers of the second kind. -/
+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
 
 /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version in a general ring
 with summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
 see `hasSum_coe_mul_geometric_of_norm_lt_one`. -/
 theorem hasSum_coe_mul_geometric_of_norm_lt_one'
     {x : R} (h : ‖x‖ < 1) :
     HasSum (fun n ↦ n * x ^ n : ℕ → R) (x * ((1 - x)⁻¹ʳ) ^ 2) := by
-  have A : 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 B : HasSum (fun (n : ℕ) ↦ x ^ n) ((1 - x)⁻¹ʳ) := hasSum_geom_series_inverse x h
-  convert! A.sub B using 1
-  · ext n
-    simp [add_mul]
-  · symm
-    calc (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ
-    _ = (1 - x)⁻¹ʳ ^ 2 - ((1 - x) * (1 - x)⁻¹ʳ) * (1 - x)⁻¹ʳ := by
-      simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]
-    _ = x * (1 - x)⁻¹ʳ ^ 2 := by noncomm_ring
+  convert! hasSum_pow_mul_geometric_of_norm_lt_one' 1 h using 1
+  · simp
+  · simp [Finset.sum_range_succ, stirlingSecond_self]
 
 /-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, version in a general ring with
 summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
@@ -548,6 +593,40 @@ 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' {r : R} (h : ‖r‖ < 1) :
+    HasSum (fun n : ℕ ↦ (n : R) ^ 2 * r ^ n) (r * (1 + r) * ((1 - r)⁻¹ʳ) ^ 3) := by
+  have h1 : ((1 - r)⁻¹ʳ) ^ 2 = (1 - r) * ((1 - r)⁻¹ʳ) ^ 3 := by
+    rw [pow_succ' _ 2, ← mul_assoc,
+      Ring.mul_inverse_cancel _ (isUnit_one_sub_of_norm_lt_one h), one_mul]
+  have h2 : r * (1 + r) * ((1 - r)⁻¹ʳ) ^ 3
+      = r * ((1 - r)⁻¹ʳ) ^ 2 + 2 * r ^ 2 * ((1 - r)⁻¹ʳ) ^ 3 := by
+    rw [h1]
+    noncomm_ring
+  simpa [h2, Finset.sum_range_succ, stirlingSecond_one_right, stirlingSecond_self] using
+    hasSum_pow_mul_geometric_of_norm_lt_one' 2 h
+
+/-- 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' {r : R} (h : ‖r‖ < 1) :
+    ∑' n : ℕ, (n : R) ^ 2 * r ^ n = r * (1 + r) * ((1 - r)⁻¹ʳ) ^ 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
+  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
+
 end MulGeometric
 
 section SummableLeGeometric

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
@@ -33,6 +34,12 @@ The Stirling numbers of the second kind, represent the number of ways to partiti
 * `Nat.stirlingSecond`: the number of ways to partition `n` distinct elements into `k` non-empty
   subsets, defined by the recursive relationship it satisfies.
 
+## Main results
+
+* `Nat.pow_eq_sum_stirlingSecond_mul_descFactorial`: every power `n ^ k` is a linear combination
+  of the descending factorials `Nat.descFactorial` with the Stirling numbers of the second kind
+  as coefficients.
+
 ## References
 
 * [Knuth, *The Art of Computer Programming*, Volume 1, §1.2.6][knuth1997]
@@ -169,4 +176,25 @@ 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]
 
+/-- Every power `n ^ k` is a linear combination of the descending factorials `n.descFactorial j`
+with the Stirling numbers of the second kind `stirlingSecond k j` as coefficients. -/
+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
+      rw [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]
+      simp [mul_left_comm]
+    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]
+    exact add_comm _ _
+
 end Nat

Mathlib/Data/Nat/Factorial/Basic.lean

@@ -374,6 +374,12 @@ lemma descFactorial_pos {n k : ℕ} : 0 < n.descFactorial k ↔ k ≤ n := by si
 
 alias ⟨_, descFactorial_of_lt⟩ := descFactorial_eq_zero_iff_lt
 
+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
+  · rw [descFactorial_succ, ← Nat.add_mul, Nat.sub_add_cancel h, Nat.mul_comm]
+  · simp [descFactorial_of_lt h]
+
 theorem add_descFactorial_eq_ascFactorial (n : ℕ) : ∀ k : ℕ,
     (n + k).descFactorial k = (n + 1).ascFactorial k
   | 0 => by rw [ascFactorial_zero, descFactorial_zero]