toReal_spectralRadius_complex_eq_norm

English

For a self-adjoint element a in a C*-algebra, the real-valued spectral radius equals ∥a∥.

Русский

Для сам-сопряженного элемента a спектральная радиус в вещественной части равна норме ∥a∥.

LaTeX

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

Lean4

/-- In a C⋆-algebra, the spectral radius of a self-adjoint element is equal to its norm.
See `IsSelfAdjoint.toReal_spectralRadius_eq_norm` for a version involving
`spectralRadius ℝ a`. -/
theorem toReal_spectralRadius_complex_eq_norm {a : A} (ha : IsSelfAdjoint a) : (spectralRadius ℂ a).toReal = ‖a‖ := by
  simp [ha.spectralRadius_eq_nnnorm]

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