The spectrum of elements in a complete normed algebra #
This file contains the basic theory for the resolvent and spectrum of a Banach algebra.
Theorems specific to complex Banach algebras, such as Gelfand's formula can be found in
Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean.
Main definitions #
spectralRadius : ℝ≥0∞: supremum of‖k‖₊for allk ∈ quasispectrum 𝕜 a
Main statements #
spectrum.isOpen_resolventSet: the resolvent set is open.spectrum.isClosed/quasispectrum.isClosed: the (quasi)spectrum is closed.spectrum.subset_closedBall_norm: the spectrum is a subset of closed disk of radius equal to the norm.spectrum.isCompact/quasispectrum.isCompact: the (quasi)spectrum is compact.spectralRadius_le_nnnorm: the spectral radius is bounded above by the norm.
Implementation notes #
spectralRadius is defined via quasispectrum rather than spectrum so that it makes sense for
non-unital normed rings too. When A is unital, quasispectrum 𝕜 a = spectrum 𝕜 a ∪ {0}
(quasispectrum_eq_spectrum_union_zero), and since 0 never increases the supremum defining
spectralRadius, spectralRadius_eq_of_unital shows this agrees with the supremum over
spectrum 𝕜 a alone. In general, we prove results for unital algebras and then transfer them to
the non-unital setting by considering the unital Banach algebra WithLp 1 (Unitization 𝕜 A).
Currently, the elementary results in this file (those that work for NormedField 𝕜) assume
CompleteSpace A, and for the non-unital material, CompleteSpace 𝕜. And in the unital case,
the results without NormOneClass A involve an unsightly ‖1‖ appearing in various places.
It is possible to remove the occurrences of ‖1‖, NormOneClass A, and to replace
CompleteSpace A with HasSummableGeomSeries A (and remove CompleteSpace 𝕜 in the
non-unital case), but it is currently partially blocked for reasons we shall now describe.
To make the substitutions, we need an instance of
HasSummableGeomSeries (WithLp 1 (Unitization 𝕜 A)) under the assumption HasSummableGeomSeries A
where A is a (possibly non-unital) normed algebra over a normed field 𝕜. If A is already
unital, then it is already possible to write this instance, but if A is non-unital, then we cannot
express HasSummableGeomSeries A because this is currently restricted to NormedRings, in part
because we have no Pow ℕ+ A instance for semigroups, making the necessary statement unpleasant to
express and work with.
The spectral radius is the supremum of the nnnorm (‖·‖₊) of elements in the
quasispectrum, coerced into an element of ℝ≥0∞.
It is also possible that quasispectrum 𝕜 a be unbounded (though not for Banach
algebras, see spectrum.isBounded/quasispectrum.isBounded, below). In this case,
spectralRadius a = ∞.
When A is unital, spectrum and quasispectrum differ only by the inclusion of 0 which does
not affect the spectral radius, so in the unital case, one may take the spectral radius to be the
supremum over the spectrum instead of the quasispectrum (see spectralRadius_eq_of_unital).
Equations
- spectralRadius 𝕜 a = ⨆ k ∈ quasispectrum 𝕜 a, ↑‖k‖₊
Instances For
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‖₊⁻¹.
For 𝕜 = ℝ or 𝕜 = ℂ, exp maps the spectrum of a into the spectrum of exp a.
Alias of spectralRadius_le_nnnorm.
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).
Equations
- φ.toContinuousLinearMap = { toLinearMap := φ.toLinearMap, cont := ⋯ }
Instances For
The equivalence between characters and algebra homomorphisms into the base field.
Equations
- WeakDual.CharacterSpace.equivAlgHom = { toFun := WeakDual.CharacterSpace.toAlgHom, invFun := fun (f : A →ₐ[𝕜] 𝕜) => ⟨f.toContinuousLinearMap, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Let S be a closed subalgebra of a Banach algebra A. If a : S is invertible in A,
and for all x : S sufficiently close to a within some filter l, x is invertible in S,
then a is invertible in S as well.
If S : Subalgebra 𝕜 A is a closed subalgebra of a Banach algebra A, then for any
x : S, the boundary of the spectrum of x relative to S is a subset of the spectrum of
↑x : A relative to A.
If S is a closed subalgebra of a Banach algebra A, then for any x : S, the boundary of
the spectrum of x relative to S is a subset of the boundary of the spectrum of ↑x : A
relative to A.
If S is a closed subalgebra of a Banach algebra A, then for any x : S, the spectrum of x
is the spectrum of ↑x : A along with the connected components of the complement of the spectrum of
↑x : A which contain an element of the spectrum of x : S.
Let S be a closed subalgebra of a Banach algebra A, and let x : S. If z is in the
spectrum of x, then the connected component of z in the complement of the spectrum of ↑x : A
is bounded (or else z actually belongs to the spectrum of ↑x : A).
Let S be a closed subalgebra of a Banach algebra A. If for x : S the complement of the
spectrum of ↑x : A is connected, then spectrum 𝕜 x = spectrum 𝕜 (x : A).
If 𝕜₁ is a normed field contained as subfield of a larger normed field 𝕜₂, and if a : A
is an element (in a possibly non-unital 𝕜₂-algebra) whose 𝕜₂ quasispectrum restricts to 𝕜₁,
then the spectral radii over each scalar field coincide.
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.
The map a ↦ spectrum ℝ≥0 a is upper hemicontinuous.
The map a ↦ quasispectrum 𝕜 a is upper hemicontinuous.
The map a ↦ quasispectrum ℝ≥0 a is upper hemicontinuous.