radius_compNeg — Mathlib

English

If ∑ ‖p_n‖ r^n converges for some r, then r is bounded by p.radius.

Русский

Если ∑ ‖p_n‖ r^n сходится, то r ограничен p.radius.

LaTeX

$$$\\text{Summable } \\sum_n \\|p_n\\| r^n \\Rightarrow r \\le p.radius.$$$

Lean4

@[simp]
theorem radius_compNeg [Nontrivial E] (p : FormalMultilinearSeries 𝕜 E F) :
    (p.compContinuousLinearMap (-(.id _ _))).radius = p.radius :=
  radius_compContinuousLinearMap_linearIsometryEquiv_eq _ (.neg 𝕜)

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