The spectrum of elements in a complete normed algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

spectral_radius : ℝ≥0∞: supremum of ‖k‖₊ for all k ∈ spectrum 𝕜 a
normed_ring.alg_equiv_complex_of_complete: 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

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.
spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius: Gelfand's formula for the spectral radius in Banach algebras over ℂ.
spectrum.nonempty: the spectrum of any element in a complex Banach algebra is nonempty.

TODO #

compute all derivatives of resolvent a.

source

noncomputable def spectral_radius (𝕜 : Type u_1) {A : Type u_2} [normed_field 𝕜] [ring A] [algebra 𝕜 A] (a : A) :

ennreal

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

spectral_radius 𝕜 a = ⨆ (k : 𝕜) (H : k ∈ spectrum 𝕜 a), ↑‖k‖₊

source

@[simp]

theorem spectrum.spectral_radius.of_subsingleton {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [subsingleton A] (a : A) :

spectral_radius 𝕜 a = 0

source

@[simp]

theorem spectrum.spectral_radius_zero {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] :

spectral_radius 𝕜 0 = 0

source

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‖₊) :

k ∈ resolvent_set 𝕜 a

source

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)

source

@[protected]

theorem spectrum.is_closed {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] (a : A) :

is_closed (spectrum 𝕜 a)

source

theorem spectrum.mem_resolvent_set_of_norm_lt_mul {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] {a : A} {k : 𝕜} (h : ‖a‖ * ‖1‖ < ‖k‖) :

k ∈ resolvent_set 𝕜 a

source

theorem spectrum.mem_resolvent_set_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‖) :

k ∈ resolvent_set 𝕜 a

source

theorem spectrum.norm_le_norm_mul_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) :

‖k‖ ≤ ‖a‖ * ‖1‖

source

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) :

‖k‖ ≤ ‖a‖

source

theorem spectrum.subset_closed_ball_norm_mul {𝕜 : 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‖ * ‖1‖)

source

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) :

spectrum 𝕜 a ⊆ metric.closed_ball 0 ‖a‖

source

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)

source

@[protected]

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)

source

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) :

spectral_radius 𝕜 a ≤ ↑‖a‖₊

source

theorem spectrum.exists_nnnorm_eq_spectral_radius_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [proper_space 𝕜] {a : A} (ha : (spectrum 𝕜 a).nonempty) :

∃ (k : 𝕜) (H : k ∈ spectrum 𝕜 a), ↑‖k‖₊ = spectral_radius 𝕜 a

source

theorem spectrum.spectral_radius_lt_of_forall_lt_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [proper_space 𝕜] {a : A} (ha : (spectrum 𝕜 a).nonempty) {r : nnreal} (hr : ∀ (k : 𝕜), k ∈ spectrum 𝕜 a → ‖k‖₊ < r) :

spectral_radius 𝕜 a < ↑r

source

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 : ℕ) :

spectral_radius 𝕜 a ≤ ↑‖a ^ (n + 1)‖₊ ^ (1 / (↑n + 1)) * ↑‖1‖₊ ^ (1 / (↑n + 1))

source

theorem spectrum.spectral_radius_le_liminf_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) :

spectral_radius 𝕜 a ≤ filter.liminf (λ (n : ℕ), ↑‖a ^ n‖₊ ^ (1 / ↑n)) filter.at_top

source

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) :

has_deriv_at (resolvent a) (-resolvent a k ^ 2) k

source

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 ≤ ‖z‖ → ‖resolvent a z‖ ≤ ε

source

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) :

has_fpower_series_on_ball (λ (z : 𝕜), ring.inverse (1 - z • a)) (λ (n : ℕ), continuous_multilinear_map.mk_pi_field 𝕜 (fin n) (a ^ n)) 0 (↑‖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‖₊⁻¹.

source

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)

source

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)⁻¹.

source

theorem spectrum.limsup_pow_nnnorm_pow_one_div_le_spectral_radius {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] (a : A) :

filter.limsup (λ (n : ℕ), ↑‖a ^ n‖₊ ^ (1 / ↑n)) filter.at_top ≤ spectral_radius ℂ a

The limsup relationship for the spectral radius used to prove spectrum.gelfand_formula.

source

theorem spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectral_radius {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] (a : A) :

filter.tendsto (λ (n : ℕ), ↑‖a ^ n‖₊ ^ (1 / ↑n)) filter.at_top (nhds (spectral_radius ℂ a))

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)

source

theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectral_radius {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] (a : A) :

filter.tendsto (λ (n : ℕ), ennreal.of_real (‖a ^ n‖ ^ (1 / ↑n))) filter.at_top (nhds (spectral_radius ℂ a))

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)

source

@[protected]

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

(spectrum ℂ a).nonempty

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

source

theorem spectrum.exists_nnnorm_eq_spectral_radius {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] (a : A) :

∃ (z : ℂ) (H : z ∈ spectrum ℂ a), ↑‖z‖₊ = spectral_radius ℂ a

In a complex Banach algebra, the spectral radius is always attained by some element of the spectrum.

source

theorem spectrum.spectral_radius_lt_of_forall_lt {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] (a : A) {r : nnreal} (hr : ∀ (z : ℂ), z ∈ spectrum ℂ a → ‖z‖₊ < r) :

spectral_radius ℂ a < ↑r

In a complex Banach algebra, if every element of the spectrum has norm strictly less than r : ℝ≥0, then the spectral radius is also strictly less than r.

source

theorem spectrum.map_polynomial_aeval {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] (a : A) (p : polynomial ℂ) :

spectrum ℂ (⇑(polynomial.aeval a) p) = (λ (k : ℂ), polynomial.eval k p) '' spectrum ℂ a

The spectral mapping theorem for polynomials in a Banach algebra over ℂ.

source

@[protected]

theorem spectrum.map_pow {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] [complete_space A] [nontrivial A] (a : A) (n : ℕ) :

spectrum ℂ (a ^ n) = (λ (x : ℂ), x ^ n) '' spectrum ℂ a

A specialization of the spectral mapping theorem for polynomials in a Banach algebra over ℂ to monic monomials.

source

theorem spectrum.algebra_map_eq_of_mem {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] (hA : ∀ {a : A}, is_unit a ↔ a ≠ 0) {a : A} {z : ℂ} (h : z ∈ spectrum ℂ a) :

⇑(algebra_map ℂ A) z = a

source

noncomputable def normed_ring.alg_equiv_complex_of_complete {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] (hA : ∀ {a : A}, is_unit a ↔ a ≠ 0) [complete_space A] :

ℂ ≃ₐ[ℂ ] 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.

Note: because normed_division_ring requires the field norm_mul' : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖, we don't use this type class and instead opt for a normed_ring in which the nonzero elements are precisely the units. This allows for the application of this isomorphism in broader contexts, e.g., to the quotient of a complex Banach algebra by a maximal ideal. In the case when A is actually a normed_division_ring, one may fill in the argument hA with the lemma is_unit_iff_ne_zero.

Equations

normed_ring.alg_equiv_complex_of_complete hA = let nt : nontrivial A := _ in {to_fun := ⇑(algebra_map ℂ A), inv_fun := λ (a : A), _.some, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem normed_ring.alg_equiv_complex_of_complete_apply {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] (hA : ∀ {a : A}, is_unit a ↔ a ≠ 0) [complete_space A] (ᾰ : ℂ) :

⇑(normed_ring.alg_equiv_complex_of_complete hA) ᾰ = ⇑(algebra_map ℂ A) ᾰ

source

@[simp]

theorem normed_ring.alg_equiv_complex_of_complete_symm_apply {A : Type u_2} [normed_ring A] [normed_algebra ℂ A] (hA : ∀ {a : A}, is_unit a ↔ a ≠ 0) [complete_space A] (a : A) :

⇑((normed_ring.alg_equiv_complex_of_complete hA).symm) a = _.some

source

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.

source

@[protected, instance]

def alg_hom.continuous_linear_map_class {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [alg_hom_class F 𝕜 A 𝕜] :

continuous_linear_map_class F 𝕜 A 𝕜

An algebra homomorphism into the base field, as a continuous linear map (since it is automatically bounded). See note [lower instance priority]

Equations

alg_hom.continuous_linear_map_class = {coe := semilinear_map_class.coe alg_hom_class.linear_map_class, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}

source

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 →ₐ[𝕜] 𝕜) :

A →L[𝕜] 𝕜

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

Equations

φ.to_continuous_linear_map = {to_linear_map := {to_fun := φ.to_linear_map.to_fun, map_add' := _, map_smul' := _}, cont := _}

source

@[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] (φ : A →ₐ[𝕜] 𝕜) :

⇑(φ.to_continuous_linear_map) = ⇑φ

source

theorem alg_hom.norm_apply_le_self_mul_norm_one {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [alg_hom_class F 𝕜 A 𝕜] (f : F) (a : A) :

‖⇑f a‖ ≤ ‖a‖ * ‖1‖

source

theorem alg_hom.norm_apply_le_self {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [normed_field 𝕜] [normed_ring A] [normed_algebra 𝕜 A] [complete_space A] [norm_one_class A] [alg_hom_class F 𝕜 A 𝕜] (f : F) (a : A) :

‖⇑f a‖ ≤ ‖a‖

source

@[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 →ₐ[𝕜] 𝕜) :

‖φ.to_continuous_linear_map ‖ = 1

source

def weak_dual.character_space.equiv_alg_hom {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [complete_space A] [normed_algebra 𝕜 A] :

↥(weak_dual.character_space 𝕜 A) ≃ (A →ₐ[𝕜] 𝕜)

The equivalence between characters and algebra homomorphisms into the base field.

Equations

weak_dual.character_space.equiv_alg_hom = {to_fun := weak_dual.character_space.to_alg_hom normed_algebra.to_algebra, inv_fun := λ (f : A →ₐ[𝕜] 𝕜), ⟨f.to_continuous_linear_map, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem weak_dual.character_space.equiv_alg_hom_coe {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [complete_space A] [normed_algebra 𝕜 A] (f : ↥(weak_dual.character_space 𝕜 A)) :

⇑(⇑weak_dual.character_space.equiv_alg_hom f) = ⇑f

source

@[simp]

theorem weak_dual.character_space.equiv_alg_hom_symm_coe {𝕜 : Type u_1} {A : Type u_2} [nontrivially_normed_field 𝕜] [normed_ring A] [complete_space A] [normed_algebra 𝕜 A] (f : A →ₐ[𝕜] 𝕜) :

⇑(⇑(weak_dual.character_space.equiv_alg_hom.symm) f) = ⇑f