English
For a normal (IsStarNormal) element a, the spectral radius equals the nnorm: ρ_C(a) = ∥a∥₊.
Русский
Для нормального элемента a спектральная радиус равна nnorm(a).
LaTeX
$$$$\operatorname{spectralRadius}_{\mathbb{C}}(a) = \|a\|_{+}.$$$
Lean4
theorem spectralRadius_eq_nnnorm (a : A) [IsStarNormal a] : spectralRadius ℂ a = ‖a‖₊ :=
by
refine (ENNReal.pow_right_strictMono two_ne_zero).injective ?_
have heq :
(fun n : ℕ => (‖(a⋆ * a) ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ)) =
(fun x => x ^ 2) ∘ fun n : ℕ => (‖a ^ n‖₊ : ℝ≥0∞) ^ (1 / n : ℝ) :=
by
funext n
rw [Function.comp_apply, ← rpow_natCast, ← rpow_mul, mul_comm, rpow_mul, rpow_natCast, ← coe_pow, sq, ←
nnnorm_star_mul_self, Commute.mul_pow (star_comm_self' a), star_pow]
have h₂ :=
((ENNReal.continuous_pow 2).tendsto (spectralRadius ℂ a)).comp
(spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a)
rw [← heq] at h₂
convert tendsto_nhds_unique h₂ (pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a⋆ * a))
rw [(IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, sq, nnnorm_star_mul_self, coe_mul]
