# mathlib3documentation

analysis.normed_space.spectrum

# 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.
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
@[simp]
theorem spectrum.spectral_radius.of_subsingleton {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] [subsingleton A] (a : A) :
= 0
@[simp]
theorem spectrum.spectral_radius_zero {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] :
= 0
theorem spectrum.mem_resolvent_set_of_spectral_radius_lt {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] {a : A} {k : 𝕜} (h : < k‖₊) :
k
theorem spectrum.is_open_resolvent_set {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
@[protected]
theorem spectrum.is_closed {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : A) :
theorem spectrum.mem_resolvent_set_of_norm_lt_mul {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] {a : A} {k : 𝕜} (h : a * 1 < k) :
k
theorem spectrum.mem_resolvent_set_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_mul_of_mem {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] {a : A} {k : 𝕜} (hk : k a) :
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_mul {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (a : 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) :
@[protected]
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.exists_nnnorm_eq_spectral_radius_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] [proper_space 𝕜] {a : A} (ha : (spectrum 𝕜 a).nonempty) :
(k : 𝕜) (H : k a), k‖₊ =
theorem spectrum.spectral_radius_lt_of_forall_lt_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] [proper_space 𝕜] {a : A} (ha : (spectrum 𝕜 a).nonempty) {r : nnreal} (hr : (k : 𝕜), k a k‖₊ < r) :
< r
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)) * 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
theorem spectrum.norm_resolvent_le_forall {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] (a : A) (ε : ) (H : ε > 0) :
(R : ) (H : R > 0), (z : 𝕜), R z z ε
theorem spectrum.has_fpower_series_on_ball_inverse_one_sub_smul (𝕜 : Type u_1) {A : Type u_2} [normed_ring A] [ A] (a : A) :
has_fpower_series_on_ball (λ (z : 𝕜), ring.inverse (1 - z a)) (λ (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‖₊⁻¹.

theorem spectrum.is_unit_one_sub_smul_of_lt_inv_radius {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] {a : A} {z : 𝕜} (h : z‖₊ < a)⁻¹) :
is_unit (1 - z a)
theorem spectrum.differentiable_on_inverse_one_sub_smul {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] {a : A} {r : nnreal} (hr : r < a)⁻¹) :
(λ (z : 𝕜), ring.inverse (1 - z a)) 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)

@[protected]
theorem spectrum.nonempty {A : Type u_2} [normed_ring A] [ A] [nontrivial A] (a : A) :

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

theorem spectrum.exists_nnnorm_eq_spectral_radius {A : Type u_2} [normed_ring A] [ A] [nontrivial A] (a : A) :
(z : ) (H : z a),

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

theorem spectrum.spectral_radius_lt_of_forall_lt {A : Type u_2} [normed_ring A] [ A] [nontrivial A] (a : A) {r : nnreal} (hr : (z : ), z z‖₊ < 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.

theorem spectrum.map_polynomial_aeval {A : Type u_2} [normed_ring A] [ A] [nontrivial A] (a : A) (p : polynomial ) :
( p) = (λ (k : ), p) ''

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

@[protected]
theorem spectrum.map_pow {A : Type u_2} [normed_ring A] [ A] [nontrivial A] (a : A) (n : ) :
(a ^ n) = (λ (x : ), x ^ n) ''

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

theorem spectrum.algebra_map_eq_of_mem {A : Type u_2} [normed_ring A] [ A] (hA : {a : A}, a 0) {a : A} {z : } (h : z ) :
A) z = a
noncomputable def normed_ring.alg_equiv_complex_of_complete {A : Type u_2} [normed_ring A] [ A] (hA : {a : A}, a 0)  :

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
@[simp]
theorem normed_ring.alg_equiv_complex_of_complete_apply {A : Type u_2} [normed_ring A] [ A] (hA : {a : A}, a 0) (ᾰ : ) :
= A)
@[simp]
theorem normed_ring.alg_equiv_complex_of_complete_symm_apply {A : Type u_2} [normed_ring A] [ A] (hA : {a : A}, a 0) (a : A) :
theorem spectrum.exp_mem_exp {𝕜 : Type u_1} {A : Type u_2} [is_R_or_C 𝕜] [normed_ring A] [ A] (a : A) {z : 𝕜} (hz : z a) :
exp 𝕜 z (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} {F : Type u_3} [normed_field 𝕜] [normed_ring A] [ A] [ A 𝕜] :
𝕜

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

Equations
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.coe_to_continuous_linear_map {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [normed_ring A] [ A] (φ : A →ₐ[𝕜] 𝕜) :
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] [ A] [ A 𝕜] (f : F) (a : A) :
theorem alg_hom.norm_apply_le_self {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [normed_field 𝕜] [normed_ring A] [ A] [ A 𝕜] (f : F) (a : A) :
@[simp]
theorem alg_hom.to_continuous_linear_map_norm {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] (φ : A →ₐ[𝕜] 𝕜) :
def weak_dual.character_space.equiv_alg_hom {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] :
(A →ₐ[𝕜] 𝕜)

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

Equations
@[simp]
theorem weak_dual.character_space.equiv_alg_hom_coe {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] (f : ) :
@[simp]
theorem weak_dual.character_space.equiv_alg_hom_symm_coe {𝕜 : Type u_1} {A : Type u_2} [normed_ring A] [ A] (f : A →ₐ[𝕜] 𝕜) :