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 #
spectral_radius : ℝ≥0∞
: supremum of∥k∥₊
for allk ∈ spectrum 𝕜 a
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.spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius
: Gelfand's formula for the spectral radius in Banach algebras overℂ
.spectrum.nonempty
: the spectrum of any element in a complex Banach algebra is nonempty.normed_division_ring.alg_equiv_complex_of_complete
: Gelfand-Mazur theorem For a complex Banach division algebra, the naturalalgebra_map ℂ A
is an algebra isomorphism whose inverse is given by selecting the (unique) element ofspectrum ℂ a
TODO #
- compute all derivatives of
resolvent a
.
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, 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 = ∞
.
In a Banach algebra A
over a nontrivially normed field 𝕜
, for any a : A
the
power series with coefficients a ^ n
represents the function (1 - z • a)⁻¹
in a disk of
radius ∥a∥₊⁻¹
.
In a Banach algebra A
over 𝕜
, for a : A
the function λ z, (1 - z • a)⁻¹
is
differentiable on any closed ball centered at zero of radius r < (spectral_radius 𝕜 a)⁻¹
.
The limsup
relationship for the spectral radius used to prove spectrum.gelfand_formula
.
Gelfand's formula: Given an element a : A
of a complex Banach algebra, the
spectral_radius
of a
is the limit of the sequence ∥a ^ n∥₊ ^ (1 / n)
Gelfand's formula: Given an element a : A
of a complex Banach algebra, the
spectral_radius
of a
is the limit of the sequence ∥a ^ n∥₊ ^ (1 / n)
In a (nontrivial) complex Banach algebra, every element has nonempty spectrum.
Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebra_map ℂ A
is an algebra isomorphism whose inverse is given by selecting the (unique) element of
spectrum ℂ a
. In addition, algebra_map_isometry
guarantees this map is an isometry.
For 𝕜 = ℝ
or 𝕜 = ℂ
, exp 𝕜
maps the spectrum of a
into the spectrum of exp 𝕜 a
.
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).
Equations
- alg_hom.continuous_linear_map_class = {coe := semilinear_map_class.coe alg_hom_class.linear_map_class, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).
Equations
- φ.to_continuous_linear_map = {to_linear_map := {to_fun := φ.to_linear_map.to_fun, map_add' := _, map_smul' := _}, cont := _}