Gelfand's formula and other results on the spectrum in complex Banach algebras #
This file contains results on the spectrum of elements in a complex Banach algebra, including Gelfand's formula and the Gelfand-Mazur theorem and the fact that every element in a complex Banach algebra has nonempty spectrum.
Main results #
spectrum.hasDerivAt_resolvent: the resolvent function is differentiable on the resolvent set.spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius: 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.NormedRing.algEquivComplexOfComplete: Gelfand-Mazur theorem For a complex Banach division algebra, the naturalalgebraMap โ Ais an algebra isomorphism whose inverse is given by selecting the (unique) element ofspectrum โ a
In a Banach algebra A over ๐, for a : A the function fun z โฆ (1 - z โข a)โปยน is
differentiable on any closed ball centered at zero of radius r < (spectralRadius ๐ 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
spectralRadius of a is the limit of the sequence โa ^ nโโ ^ (1 / n).
Alias of spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius.
Gelfand's formula: Given an element a : A of a complex Banach algebra, the
spectralRadius 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
spectralRadius of a is the limit of the sequence โa ^ nโโ ^ (1 / n).
In a (nontrivial) complex Banach algebra, every element has nonempty spectrum.
In a complex Banach algebra, the spectral radius is always attained by some element of the spectrum.
In a complex Banach algebra, if every element of the spectrum has norm strictly less than
r : โโฅ0, then the spectral radius is also strictly less than r.
The spectral mapping theorem for polynomials in a Banach algebra over โ.
A specialization of the spectral mapping theorem for polynomials in a Banach algebra over โ
to monic monomials.
Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebraMap โ A
is an algebra isomorphism whose inverse is given by selecting the (unique) element of
spectrum โ a. In addition, algebraMap_isometry guarantees this map is an isometry.
Note: because NormedDivisionRing requires the field norm_mul : โ a b, โa * bโ = โaโ * โbโ, we
don't use this type class and instead opt for a NormedRing in which the nonzero elements are
precisely the units. This allows for the application of this isomorphism in broader contexts, e.g.,
to the quotient of a complex Banach algebra by a maximal ideal. In the case when A is actually a
NormedDivisionRing, one may fill in the argument hA with the lemma isUnit_iff_ne_zero.
Equations
- NormedRing.algEquivComplexOfComplete hA = { toFun := โ(algebraMap โ A), invFun := fun (a : A) => โฏ.some, left_inv := โฏ, right_inv := โฏ, map_mul' := โฏ, map_add' := โฏ, commutes' := โฏ }