Commit 2026-08-13 13:53 d16a3fcc

feat(Analysis/SpecificLimits/Normed): the sum ∑' n, n ^ k * r ^ n via Stirling numbers (#41498) For ‖r‖ < 1, compute ∑' n : ℕ, n ^ k * r ^ n as the finite sum ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j / (1 - r) ^ (j + 1), where S(k, j) are the Stirling numbers of the second kind. Motivation: a special case of tsum_sq_mul_geometric_of_norm_lt_one over ℂ was proved in the FLT project and is generalized here to match the surrounding Mathlib API; the private FLT lemma can then be replaced by this one. Main additions to Normed.lean:

• The general power formula:
  • hasSum_pow_mul_geometric_of_norm_lt_one' / tsum_pow_mul_geometric_of_norm_lt_one': for ‖r‖ < 1 in a general ring, ∑' n, n ^ k * r ^ n = ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1).
  • hasSum_pow_mul_geometric_of_norm_lt_one / tsum_pow_mul_geometric_of_norm_lt_one: the same in a field, with / (1 - r) ^ (j + 1).
• The descFactorial special case that supplies each term of that sum:
  • hasSum_descFactorial_mul_geometric_of_norm_lt_one' / tsum_descFactorial_mul_geometric_of_norm_lt_one': for ‖r‖ < 1 in a general ring, ∑' n, n.descFactorial j * r ^ n = j ! * r ^ j * ((1 - r)⁻¹ʳ) ^ (j + 1).
  • hasSum_descFactorial_mul_geometric_of_norm_lt_one / tsum_descFactorial_mul_geometric_of_norm_lt_one: the field versions, with / (1 - r) ^ (j + 1). Additions to other files:
• Combinatorics/Enumerative/Stirling.lean: Nat.pow_eq_sum_stirlingSecond_mul_descFactorial, expressing every power n ^ k as a linear combination n ^ k = ∑ j ∈ range (k + 1), stirlingSecond k j * n.descFactorial j.
• Data/Nat/Factorial/Basic.lean: Nat.descFactorial_mul_self, the identity n.descFactorial j * n = n.descFactorial (j + 1) + j * n.descFactorial j, used in the induction proving the Stirling result above. Other changes:
• summable_pow_mul_geometric_of_norm_lt_one (statement unchanged) is now a one-line consequence of the general formula; its previous proof via ascPochhammer is deleted, so the RingTheory.Polynomial.Pochhammer import is no longer needed.
• The statement of summable_descFactorial_mul_geometric_of_norm_lt_one changes from the shifted summand (n + k).descFactorial k * r ^ n to n.descFactorial k * r ^ n, to match the new hasSum/tsum lemmas. It had no other uses in Mathlib, and the shifted form is recoverable in one line from summable_choose_mul_geometric_of_norm_lt_one.
• The proof of hasSum_coe_mul_geometric_of_norm_lt_one' (k = 1) is simplified using the general formula, and the k = 2 case is added: ∑' n, n ^ 2 * r ^ n = r * (1 + r) / (1 - r) ^ 3 (hasSum_sq_mul_geometric_of_norm_lt_one' and the three companion lemmas).
• The redundant imports mentioned above have now been removed; this required import edits in 8 dependent files that had relied on them transitively. AI Disclosure: this code originated in the FLT project, where an initial version was written by William Coram and Samuel Yin with AI assistance (Claude, later cleaned up with Codex). It has since been substantially rewritten for this PR; little of the original generated code remains.