mathlib documentation

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.

Main definitions #

Main statements #

TODO #

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

Equations
theorem spectrum.mem_resolvent_set_of_spectral_radius_lt {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] {a : A} {k : 𝕜} (h : spectral_radius 𝕜 a < k∥₊) :
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) :
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] [norm_one_class A] {a : A} {k : 𝕜} (h : a < k) :
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] [norm_one_class 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] [norm_one_class A] (a : A) :
theorem spectrum.is_bounded {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] (a : A) :
theorem spectrum.is_compact {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] [proper_space 𝕜] (a : 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] [norm_one_class 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] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] (a : A) (n : ) :
spectral_radius 𝕜 a a ^ (n + 1)∥₊ ^ (1 / (n + 1))
theorem spectrum.has_deriv_at_resolvent {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] {a : A} {k : 𝕜} (hk : k resolvent_set 𝕜 a) :
theorem spectrum.norm_resolvent_le_forall {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] (a : A) (ε : ) (H : ε > 0) :
∃ (R : ) (H : R > 0), ∀ (z : 𝕜), R zresolvent a z ε
theorem spectrum.has_fpower_series_on_ball_inverse_one_sub_smul (𝕜 : Type u_1) {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] (a : A) :

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∥₊⁻¹.

theorem spectrum.is_unit_one_sub_smul_of_lt_inv_radius {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] {a : A} {z : 𝕜} (h : z∥₊ < (spectral_radius 𝕜 a)⁻¹) :
is_unit (1 - z a)
theorem spectrum.differentiable_on_inverse_one_sub_smul {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] {a : A} {r : nnreal} (hr : r < (spectral_radius 𝕜 a)⁻¹) :
differentiable_on 𝕜 (λ (z : 𝕜), ring.inverse (1 - z a)) (metric.closed_ball 0 r)

In a Banach algebra A over 𝕜, for a : A the function λ z, (1 - z • a)⁻¹ is differentiable on any closed ball centered at zero of radius r < (spectral_radius 𝕜 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 spectral_radius 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 spectral_radius of a is the limit of the sequence ∥a ^ n∥₊ ^ (1 / n)

theorem spectrum.nonempty {A : Type u_1} [normed_ring A] [normed_algebra A] [complete_space A] [nontrivial A] (a : A) :

In a (nontrivial) complex Banach algebra, every element has nonempty spectrum.

theorem spectrum.algebra_map_eq_of_mem {A : Type u_2} [normed_division_ring A] [normed_algebra A] {a : A} {z : } (h : z spectrum a) :

Gelfand-Mazur theorem: For a complex Banach division algebra, the natural algebra_map ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a. In addition, algebra_map_isometry guarantees this map is an isometry.

Equations
theorem spectrum.exp_mem_exp {𝕜 : Type u_1} {A : Type u_2} [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] (a : A) {z : 𝕜} (hz : z spectrum 𝕜 a) :
exp 𝕜 z spectrum 𝕜 (exp 𝕜 a)

For 𝕜 = ℝ or 𝕜 = ℂ, exp 𝕜 maps the spectrum of a into the spectrum of exp 𝕜 a.

@[protected, instance]
def alg_hom.continuous_linear_map_class {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] :
continuous_linear_map_class (A →ₐ[𝕜] 𝕜) 𝕜 A 𝕜

An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded).

Equations
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] [norm_one_class 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.coe_to_continuous_linear_map {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) :
@[simp]
theorem alg_hom.to_continuous_linear_map_norm {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] (φ : A →ₐ[𝕜] 𝕜) :