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 #
spectralRadius : ℝ≥0∞
: supremum of‖k‖₊
for allk ∈ spectrum 𝕜 a
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
Main statements #
spectrum.isOpen_resolventSet
: the resolvent set is open.spectrum.isClosed
: the spectrum is closed.spectrum.subset_closedBall_norm
: the spectrum is a subset of closed disk of radius equal to the norm.spectrum.isCompact
: the spectrum is compact.spectrum.spectralRadius_le_nnnorm
: the spectral radius is bounded above by the norm.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.
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, 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 = ∞
.
Equations
- spectralRadius 𝕜 a = ⨆ k ∈ spectrum 𝕜 a, ↑‖k‖₊
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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 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)
.
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
- One or more equations did not get rendered due to their size.
Instances For
For 𝕜 = ℝ
or 𝕜 = ℂ
, exp 𝕜
maps the spectrum of a
into the spectrum of exp 𝕜 a
.
Equations
- ⋯ = ⋯
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).
Equations
- φ.toContinuousLinearMap = let __src := φ.toLinearMap; { toLinearMap := __src, cont := ⋯ }
Instances For
The equivalence between characters and algebra homomorphisms into the base field.
Equations
Instances For
If 𝕜₁
is a normed field contained as subfield of a larger normed field 𝕜₂
, and if a : A
is an element whose 𝕜₂
spectrum restricts to 𝕜₁
, then the spectral radii over each scalar
field coincide.