The spectrum of elements in a complete normed algebra #
This file contains the basic theory for the resolvent and spectrum of a Banach algebra.
Main definitions #
Main statements #
spectrum.is_open_resolvent_set: the resolvent set is open.
spectrum.is_closed: the spectrum is closed.
spectrum.subset_closed_ball_norm: the spectrum is a subset of closed disk of radius equal to the norm.
spectrum.is_compact: the spectrum is compact.
spectrum.spectral_radius_le_nnnorm: the spectral radius is bounded above by the norm.
spectrum.has_deriv_at_resolvent: the resolvent function is differentiable on the resolvent set.
- after we have Liouville's theorem, prove that the spectrum is nonempty when the scalar field is ℂ.
- compute all derivatives of
The spectral radius is the supremum of the
∥⬝∥₊) of elements in the spectrum,
coerced into an element of
ℝ≥0∞. Note that it is possible for
spectrum 𝕜 a = ∅. In this
spectral_radius a = 0. It is also possible that
spectrum 𝕜 a be unbounded (though
not for Banach algebras, see
spectrum.is_bounded, below). In this case,
spectral_radius a = ∞.
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).