mathlibdocumentation

analysis.normed_space.spectrum

The spectrum of elements in a complete normed algebra #

This file contains the basic theory for the resolvent and spectrum of a Banach algebra.

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] [ 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 = ∞.

Equations
theorem spectrum.is_open_resolvent_set {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
theorem spectrum.is_closed {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
theorem spectrum.mem_resolvent_of_norm_lt {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] {a : A} {k : 𝕜} (h : a < k) :
k
theorem spectrum.norm_le_norm_of_mem {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] {a : A} {k : 𝕜} (hk : k a) :
theorem spectrum.subset_closed_ball_norm {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
a
theorem spectrum.is_bounded {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
theorem spectrum.is_compact {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] [proper_space 𝕜] (a : A) :
theorem spectrum.spectral_radius_le_nnnorm {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
theorem spectrum.spectral_radius_le_pow_nnnorm_pow_one_div {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) (n : ) :
a ^ (n + 1)∥₊ ^ (1 / (n + 1))
theorem spectrum.has_deriv_at_resolvent {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] {a : A} {k : 𝕜} (hk : k ) :
(- 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] [ A] (φ : A →ₐ[𝕜] 𝕜) (ᾰ : A) :
= φ ᾰ
def alg_hom.to_continuous_linear_map {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (φ : A →ₐ[𝕜] 𝕜) :
A →L[𝕜] 𝕜

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] [ A] (φ : A →ₐ[𝕜] 𝕜) (ᾰ : A) :
= φ ᾰ
theorem alg_hom.continuous {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (φ : A →ₐ[𝕜] 𝕜) :
@[simp]
theorem alg_hom.to_continuous_linear_map_norm {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] (φ : A →ₐ[𝕜] 𝕜) :