English
For any natural k and any r with ∥r∥ < 1, the sum ∑_{n≥0} n^k r^n converges and equals a polynomial in r divided by (1 − r)^{k+1}. In particular, for k = 1, ∑_{n≥0} n r^n = r/(1 − r)^2.
Русский
Для любого k ∈ ℕ и r с ∥r∥ < 1 сумма ∑ n^k r^n сходится и равна дроби, зависящей от r, деленной на (1 − r)^{k+1}. В частности, для k = 1: ∑ n r^n = r/(1 − r)^2.
LaTeX
$$\|r\| < 1 ⇒ ∑_{n=0}^{∞} n^k r^n = P_k(r) / (1 - r)^{k+1} for some polynomial P_k$$
Lean4
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 omega
simp [P, ascPochhammer_nat_eq_descFactorial, this]
conv_lhs => rw [A, mP.as_sum, dP]
simp [eval_finset_sum]
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]
