exists_nnnorm_eq_spectralRadius_of_nonempty

English

If (σ a) is nonempty, there exists k ∈ σ a such that |k| equals the spectral radius of a.

Русский

Если спектр непуст, то существует k ∈ σ a такой, что |k| равняется спектральному радиусу a.

LaTeX

$$If (σ a).Nonempty, then ∃ k ∈ σ a, |k| = spectralRadius 𝕜 a.$$

Lean4

theorem exists_nnnorm_eq_spectralRadius_of_nonempty [ProperSpace 𝕜] {a : A} (ha : (σ a).Nonempty) :
    ∃ k ∈ σ a, (‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a :=
  by
  obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn
  exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩

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