spectralRadius_eq_nnnorm — Mathlib

English

In a C*-algebra, the spectral radius of a self-adjoint element equals its norm: ρ_C(a) = ∥a∥₊.

Русский

В C*-алгебре спектральная радиус сам-сопряженного элемента равна его норме: ρ_C(a) = ∥a∥₊.

LaTeX

$$$$\operatorname{spectralRadius}_{\mathbb{C}}(a) = \|a\|_{+}.$$$$

Lean4

theorem spectralRadius_eq_nnnorm {a : A} (ha : IsSelfAdjoint a) : spectralRadius ℂ a = ‖a‖₊ :=
  by
  have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
  refine tendsto_nhds_unique ?_ hconst
  convert
    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
      (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using
    1
  refine funext fun n => ?_
  rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]
  simp

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