diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index deecc84a1b3899..c9bbb94e928eef 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/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,38 +477,93 @@ 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`, @@ -517,18 +571,9 @@ 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 diff --git a/Mathlib/Combinatorics/Enumerative/Stirling.lean b/Mathlib/Combinatorics/Enumerative/Stirling.lean index 251fbe7940ceb5..2a77d536abe1e6 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 @@ -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 diff --git a/Mathlib/Data/Nat/Factorial/Basic.lean b/Mathlib/Data/Nat/Factorial/Basic.lean index 092a314777028b..cbaf426ba261aa 100644 --- a/Mathlib/Data/Nat/Factorial/Basic.lean +++ b/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]