Theorems · Definition · functional analysis

spectralRadius

(𝕜 : Type u_1) → {A : Type u_2} → [inst : NormedField 𝕜] → [inst_1 : Ring A] → [Algebra 𝕜 A] → A → ENNReal

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 = ∞.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

36 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldRingAlgebra