radius — Mathlib

English

If p_n = 0 eventually, then radius(p) = ∞.

Русский

Если последовательность p_n равна нулю после некоторого момента, тогда радиус бесконечен.

LaTeX

$$radius_eq_top_of_eventually_eq_zero (h) : p.radius = ∞$$

Lean4

/-- The radius of a formal multilinear series is the largest `r` such that the sum `Σ ‖pₙ‖ ‖y‖ⁿ`
converges for all `‖y‖ < r`. This implies that `Σ pₙ yⁿ` converges for all `‖y‖ < r`, but these
definitions are *not* equivalent in general. -/
def radius (p : FormalMultilinearSeries 𝕜 E F) : ℝ≥0∞ :=
  ⨆ (r : ℝ≥0) (C : ℝ) (_ : ∀ n, ‖p n‖ * (r : ℝ) ^ n ≤ C), (r : ℝ≥0∞)

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