English
The spectral radius of a is defined as the supremum of the nnnorms of elements of its spectrum, embedded in ℝ≥0∞.
Русский
Спектральный радиус a — супремум nnnorm элементов спектра a, отображённый в ℝ≥0∞.
LaTeX
$$$\operatorname{spectralRadius}(\mathbb{K}, a) = \sup\{ \|k\|_{+} : k \in \mathrm{spectrum}(\mathbb{K}, a) \}.$$$
Lean4
/-- The *spectral radius* is the supremum of the `nnnorm` (`‖·‖₊`) of elements in the spectrum,
coerced into an element of `ℝ≥0∞`. Note that it is possible for `spectrum 𝕜 a = ∅`. In this
case, `spectralRadius a = 0`. It is also possible that `spectrum 𝕜 a` be unbounded (though
not for Banach algebras, see `spectrum.isBounded`, below). In this case,
`spectralRadius a = ∞`. -/
noncomputable def spectralRadius (𝕜 : Type*) {A : Type*} [NormedField 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) : ℝ≥0∞ :=
⨆ k ∈ spectrum 𝕜 a, ‖k‖₊
