summable — Mathlib

English

If for all real r≥0 the series ∑ ‖p_n‖ r^n converges, then radius(p) = ∞.

Русский

Если для всех r≥0 сумма ∑ ‖p_n‖ r^n сходится, то radius(p) = ∞.

LaTeX

$$$\\big( \\forall r \\ge 0:\\; \\sum_{n} \\|p_n\\| r^n < \\infty \\big) \\Rightarrow p.radius = \\infty.$$$

Lean4

protected theorem summable [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E}
    (hx : x ∈ EMetric.ball (0 : E) p.radius) : Summable fun n : ℕ => p n fun _ => x :=
  (p.summable_norm_apply hx).of_norm

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