toReal_spectralRadius_eq_norm — Mathlib

English

If a is self-adjoint in A, then the real spectral radius of a equals the norm of a, i.e., (spectralRadius ℝ a).toReal = ‖a‖.

Русский

Если a само-сопряжённый элемент, то вещественный спектральный радиус a равен норме a: (spectralRadius ℝ a).toReal = ‖a‖.

LaTeX

$$(\\text{spectralRadius} \\; \\mathbb{R} \\; a)^{\\mathrm{toReal}} = \\|a\\|$$

Lean4

theorem toReal_spectralRadius_eq_norm {a : A} (ha : IsSelfAdjoint a) : (spectralRadius ℝ a).toReal = ‖a‖ := by
  simp [ha.spectrumRestricts.spectralRadius_eq, ha.spectralRadius_eq_nnnorm]

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