summable_norm_pow_mul_geometric_div_one_sub

English

The same summability holds when the denominator is 1 − r^n with the same hypotheses.

Русский

Та же сумма сходится, когда в знаменателе 1 − r^n при тех же предположениях.

LaTeX

$$$$ \text{Summable} \; f(n) = \frac{n^{k} r^{n}}{1 - r^{n}} \text{ при } \|r\|<1. $$$$

Lean4

theorem summable_norm_pow_mul_geometric_div_one_sub (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
    Summable fun n : ℕ ↦ n ^ k * r ^ n / (1 - r ^ n) :=
  by
  simp only [div_eq_mul_one_div (_ * _ ^ _)]
  apply
    Summable.mul_tendsto_const (c := 1 / (1 - 0)) (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
  simpa only [Nat.cofinite_eq_atTop] using
    tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)

Похожие утверждения