sum — Mathlib

English

If the series ∑ ‖p_n‖ r^n is summable, then r ≤ radius(p).

Русский

Если сумма ∑ ‖p_n‖ r^n сходится, тогда r меньше или равен радиусу p.

LaTeX

$$Summable (λ n, ‖p n‖ * (r : ℝ) ^ n) → ↑r ≤ radius(p)$$

Lean4

/-- Given a formal multilinear series `p` and a vector `x`, then `p.sum x` is the sum `Σ pₙ xⁿ`. A
priori, it only behaves well when `‖x‖ < p.radius`. -/
protected def sum (p : FormalMultilinearSeries 𝕜 E F) (x : E) : F :=
  ∑' n : ℕ, p n fun _ => x

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