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 โ A
is 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' := โฏ }