summable_norm_mul_pow — Mathlib

English

For any x in the ball of radius p.radius, the series ∑ ‖p_n fun _ => x‖ converges.

Русский

Для любого x в шаре радиуса p.radius последовательность ∑ ‖p_n fun _ => x‖ сходится.

LaTeX

$$$x \\in \\mathrm{EMetric.ball}(0, p.radius) \\Rightarrow \\sum_{n} \\|p_n( x )\\| < \\infty.$$$

Lean4

theorem summable_norm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : ↑r < p.radius) :
    Summable fun n : ℕ => ‖p n‖ * (r : ℝ) ^ n :=
  by
  obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h
  exact .of_nonneg_of_le (fun _ ↦ by positivity) hp ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)

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