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 ∈ spectrum 𝕜 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.
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
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
.
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 whose 𝕜₂
spectrum restricts to 𝕜₁
, then the spectral radii over each scalar
field coincide.