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 #
spectral_radius : ℝ≥0∞: supremum of∥k∥₊for allk ∈ spectrum 𝕜 a
Main statements #
spectrum.is_open_resolvent_set: the resolvent set is open.spectrum.is_closed: the spectrum is closed.spectrum.subset_closed_ball_norm: the spectrum is a subset of closed disk of radius equal to the norm.spectrum.is_compact: the spectrum is compact.spectrum.spectral_radius_le_nnnorm: the spectral radius is bounded above by the norm.spectrum.has_deriv_at_resolvent: the resolvent function is differentiable on the resolvent set.
TODO #
- after we have Liouville's theorem, prove that the spectrum is nonempty when the scalar field is ℂ.
- compute all derivatives of
resolvent a.
noncomputable
def
spectral_radius
(𝕜 : Type u_1)
{A : Type u_2}
[normed_field 𝕜]
[ring A]
[algebra 𝕜 A]
(a : 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, spectral_radius a = 0. It is also possible that spectrum 𝕜 a be unbounded (though
not for Banach algebras, see spectrum.is_bounded, below). In this case,
spectral_radius a = ∞.
theorem
spectrum.is_open_resolvent_set
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A) :
is_open (resolvent_set 𝕜 a)
theorem
spectrum.is_closed
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A) :
theorem
spectrum.mem_resolvent_of_norm_lt
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
{a : A}
{k : 𝕜}
(h : ∥a∥ < ∥k∥) :
k ∈ resolvent_set 𝕜 a
theorem
spectrum.norm_le_norm_of_mem
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
{a : A}
{k : 𝕜}
(hk : k ∈ spectrum 𝕜 a) :
theorem
spectrum.subset_closed_ball_norm
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A) :
spectrum 𝕜 a ⊆ metric.closed_ball 0 ∥a∥
theorem
spectrum.is_bounded
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A) :
metric.bounded (spectrum 𝕜 a)
theorem
spectrum.is_compact
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
[proper_space 𝕜]
(a : A) :
is_compact (spectrum 𝕜 a)
theorem
spectrum.spectral_radius_le_nnnorm
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A) :
spectral_radius 𝕜 a ≤ ↑∥a∥₊
theorem
spectrum.spectral_radius_le_pow_nnnorm_pow_one_div
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(a : A)
(n : ℕ) :
theorem
spectrum.has_deriv_at_resolvent
{𝕜 : Type u_1}
{A : Type u_2}
[nondiscrete_normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
{a : A}
{k : 𝕜}
(hk : k ∈ resolvent_set 𝕜 a) :
has_deriv_at (resolvent a) (-resolvent a k ^ 2) k
@[simp]
theorem
alg_hom.to_continuous_linear_map_coe_apply
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(φ : A →ₐ[𝕜] 𝕜)
(ᾰ : A) :
⇑↑(φ.to_continuous_linear_map) ᾰ = ⇑φ ᾰ
def
alg_hom.to_continuous_linear_map
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(φ : A →ₐ[𝕜] 𝕜) :
An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).
Equations
@[simp]
theorem
alg_hom.to_continuous_linear_map_apply
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(φ : A →ₐ[𝕜] 𝕜)
(ᾰ : A) :
⇑(φ.to_continuous_linear_map) ᾰ = ⇑φ ᾰ
theorem
alg_hom.continuous
{𝕜 : Type u_1}
{A : Type u_2}
[normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
(φ : A →ₐ[𝕜] 𝕜) :
@[simp]
theorem
alg_hom.to_continuous_linear_map_norm
{𝕜 : Type u_1}
{A : Type u_2}
[nondiscrete_normed_field 𝕜]
[normed_ring A]
[normed_algebra 𝕜 A]
[complete_space A]
[norm_one_class A]
(φ : A →ₐ[𝕜] 𝕜) :