summable_norm_pow_mul_geometric_of_norm_lt_one

English

For any r with ∥r∥ < 1, the series ∑ ∥r^n∥ is summable.

Русский

Для любого r с ∥r∥ < 1 ряд ∥r^n∥ суммируем.

LaTeX

$$∥r∥ < 1 ⇒ Summable (fun n => ∥r^n∥)$$

Lean4

theorem summable_norm_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) :
    Summable fun n : ℕ ↦ ‖((n : R) ^ k * r ^ n : R)‖ :=
  by
  simp only [← cast_pow]
  exact summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr (isBigO_refl _ _)

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