summable_nnnorm_mul_pow — Mathlib

English

If radius is infinite, then for every r>0 the series ∑ ‖p_n‖ r^n converges; conversely, if that holds for all r, radius is infinite.

Русский

Если радиус бесконечен, тогда для каждого r>0 ряд ∑ ‖p_n‖ r^n сходится; наоборот, если сходится для всех r, то радиус бесконечен.

LaTeX

$$$p.radius = \\infty \\;\\Leftrightarrow\\; \\forall r>0, \\; \\sum_n \\|p_n\\| r^n < \\infty.$$$

Lean4

theorem summable_nnnorm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : ↑r < p.radius) :
    Summable fun n : ℕ => ‖p n‖₊ * r ^ n := by
  rw [← NNReal.summable_coe]
  push_cast
  exact p.summable_norm_mul_pow h

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