hasSum — Mathlib

English

Radius equals ∞ iff the family of sums ∑ ‖p_n‖ r^n is summable for every r.

Русский

Радиус бесконечен тогда и только тогда, когда ∑ ‖p_n‖ r^n суммируема для всех r.

LaTeX

$$$p.radius = \\infty \\;\\Leftrightarrow\\; \\forall r\\ge 0,\\; Summable \\|p_n\\| r^n.$$$

Lean4

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

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