# 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 #

• spectralRadius : ℝ≥0∞: supremum of ‖k‖₊ for all k ∈ spectrum 𝕜 a
• NormedRing.algEquivComplexOfComplete: Gelfand-Mazur theorem For a complex Banach division algebra, the natural algebraMap ℂ A is an algebra isomorphism whose inverse is given by selecting the (unique) element of spectrum ℂ a

## Main statements #

• spectrum.isOpen_resolventSet: the resolvent set is open.
• spectrum.isClosed: the spectrum is closed.
• spectrum.subset_closedBall_norm: the spectrum is a subset of closed disk of radius equal to the norm.
• spectrum.isCompact: the spectrum is compact.
• spectrum.spectralRadius_le_nnnorm: the spectral radius is bounded above by the norm.
• spectrum.hasDerivAt_resolvent: the resolvent function is differentiable on the resolvent set.
• spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius: 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 spectralRadius (𝕜 : Type u_1) {A : Type u_2} [] [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, spectralRadius a = 0. It is also possible that spectrum 𝕜 a be unbounded (though not for Banach algebras, see spectrum.isBounded, below). In this case, spectralRadius a = ∞.

Equations
Instances For
@[simp]
theorem spectrum.SpectralRadius.of_subsingleton {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
= 0
@[simp]
theorem spectrum.spectralRadius_zero {𝕜 : Type u_1} {A : Type u_2} [] [] [] :
= 0
theorem spectrum.mem_resolventSet_of_spectralRadius_lt {𝕜 : Type u_1} {A : Type u_2} [] [] [] {a : A} {k : 𝕜} (h : < k‖₊) :
k
theorem spectrum.isOpen_resolventSet {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem spectrum.isClosed {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem spectrum.mem_resolventSet_of_norm_lt_mul {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] {a : A} {k : 𝕜} (h : a * 1 < k) :
k
theorem spectrum.mem_resolventSet_of_norm_lt {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] {a : A} {k : 𝕜} (h : a < k) :
k
theorem spectrum.norm_le_norm_mul_of_mem {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] {a : A} {k : 𝕜} (hk : k spectrum 𝕜 a) :
theorem spectrum.norm_le_norm_of_mem {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] {a : A} {k : 𝕜} (hk : k spectrum 𝕜 a) :
theorem spectrum.subset_closedBall_norm_mul {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem spectrum.subset_closedBall_norm {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] (a : A) :
spectrum 𝕜 a
theorem spectrum.isBounded {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) :
theorem spectrum.isCompact {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] (a : A) :
instance spectrum.instCompactSpace {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] (a : A) :
Equations
• =
instance spectrum.instCompactSpaceNNReal {A : Type u_3} [] [] (a : A) [CompactSpace ()] :
Equations
• =
theorem spectrum.spectralRadius_le_nnnorm {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] (a : A) :
theorem spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] {a : A} (ha : Set.Nonempty (spectrum 𝕜 a)) :
∃ k ∈ spectrum 𝕜 a, k‖₊ =
theorem spectrum.spectralRadius_lt_of_forall_lt_of_nonempty {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] [] {a : A} (ha : Set.Nonempty (spectrum 𝕜 a)) {r : NNReal} (hr : kspectrum 𝕜 a, k‖₊ < r) :
< r
theorem spectrum.spectralRadius_le_pow_nnnorm_pow_one_div (𝕜 : Type u_1) {A : Type u_2} [] [] [] [] (a : A) (n : ) :
a ^ (n + 1)‖₊ ^ (1 / (n + 1)) * 1‖₊ ^ (1 / (n + 1))
theorem spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div (𝕜 : Type u_1) {A : Type u_2} [] [] [] [] (a : A) :
Filter.liminf (fun (n : ) => a ^ n‖₊ ^ (1 / n)) Filter.atTop
theorem spectrum.hasDerivAt_resolvent {𝕜 : Type u_1} {A : Type u_2} [] [] [] {a : A} {k : 𝕜} (hk : k ) :
HasDerivAt () (- ^ 2) k
theorem spectrum.eventually_isUnit_resolvent {𝕜 : Type u_1} {A : Type u_2} [] [] [] (a : A) :
∀ᶠ (z : 𝕜) in , IsUnit ()
theorem spectrum.resolvent_isBigO_inv {𝕜 : Type u_1} {A : Type u_2} [] [] [] (a : A) :
=O[] Inv.inv
theorem spectrum.resolvent_tendsto_cobounded {𝕜 : Type u_1} {A : Type u_2} [] [] [] (a : A) :
theorem spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul (𝕜 : Type u_1) {A : Type u_2} [] [] [] (a : A) :
HasFPowerSeriesOnBall (fun (z : 𝕜) => Ring.inverse (1 - z a)) (fun (n : ) => ContinuousMultilinearMap.mkPiRing 𝕜 (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‖₊⁻¹.

theorem spectrum.isUnit_one_sub_smul_of_lt_inv_radius {𝕜 : Type u_1} {A : Type u_2} [] [] {a : A} {z : 𝕜} (h : z‖₊ < ()⁻¹) :
IsUnit (1 - z a)
theorem spectrum.differentiableOn_inverse_one_sub_smul {𝕜 : Type u_1} {A : Type u_2} [] [] [] {a : A} {r : NNReal} (hr : r < ()⁻¹) :
DifferentiableOn 𝕜 (fun (z : 𝕜) => Ring.inverse (1 - z a)) ()

In a Banach algebra A over 𝕜, for a : A the function fun z ↦ (1 - z • a)⁻¹ is differentiable on any closed ball centered at zero of radius r < (spectralRadius 𝕜 a)⁻¹.

theorem spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius {A : Type u_2} [] [] [] (a : A) :
Filter.limsup (fun (n : ) => a ^ n‖₊ ^ (1 / n)) Filter.atTop

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

theorem spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius {A : Type u_2} [] [] [] (a : A) :
Filter.Tendsto (fun (n : ) => a ^ n‖₊ ^ (1 / n)) Filter.atTop (nhds ())

Gelfand's formula: Given an element a : A of a complex Banach algebra, the spectralRadius of a is the limit of the sequence ‖a ^ n‖₊ ^ (1 / n).

theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius {A : Type u_2} [] [] [] (a : A) :
Filter.Tendsto (fun (n : ) => ENNReal.ofReal (a ^ n ^ (1 / n))) Filter.atTop (nhds ())

Gelfand's formula: Given an element a : A of a complex Banach algebra, the spectralRadius of a is the limit of the sequence ‖a ^ n‖₊ ^ (1 / n).

theorem spectrum.nonempty {A : Type u_2} [] [] [] [] (a : A) :

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

theorem spectrum.exists_nnnorm_eq_spectralRadius {A : Type u_2} [] [] [] [] (a : A) :
∃ z ∈ , z‖₊ =

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

theorem spectrum.spectralRadius_lt_of_forall_lt {A : Type u_2} [] [] [] [] (a : A) {r : NNReal} (hr : z, z‖₊ < r) :
< 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} [] [] [] [] (a : A) (p : ) :
spectrum (() p) = (fun (k : ) => ) ''

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

theorem spectrum.map_pow {A : Type u_2} [] [] [] [] (a : A) (n : ) :
spectrum (a ^ n) = (fun (x : ) => x ^ n) ''

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

theorem spectrum.algebraMap_eq_of_mem {A : Type u_2} [] [] (hA : ∀ {a : A}, a 0) {a : A} {z : } (h : z ) :
() z = a
@[simp]
theorem NormedRing.algEquivComplexOfComplete_symm_apply {A : Type u_2} [] [] (hA : ∀ {a : A}, a 0) [] (a : A) :
@[simp]
theorem NormedRing.algEquivComplexOfComplete_apply {A : Type u_2} [] [] (hA : ∀ {a : A}, a 0) [] (a : ) :
= () a
noncomputable def NormedRing.algEquivComplexOfComplete {A : Type u_2} [] [] (hA : ∀ {a : A}, a 0) [] :

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

Note: because NormedDivisionRing requires the field norm_mul' : ∀ a b, ‖a * b‖ = ‖a‖ * ‖b‖, we don't use this type class and instead opt for a NormedRing 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 NormedDivisionRing, one may fill in the argument hA with the lemma isUnit_iff_ne_zero.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem spectrum.exp_mem_exp {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (a : A) {z : 𝕜} (hz : z spectrum 𝕜 a) :
spectrum 𝕜 ()

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

def AlgHom.toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (φ : A →ₐ[𝕜] 𝕜) :
A →L[𝕜] 𝕜

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

Equations
• = let __src := ; { toLinearMap := __src, cont := }
Instances For
@[simp]
theorem AlgHom.coe_toContinuousLinearMap {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (φ : A →ₐ[𝕜] 𝕜) :
theorem AlgHom.norm_apply_le_self_mul_norm_one {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [] [] [] [] [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A) :
theorem AlgHom.norm_apply_le_self {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [] [] [] [] [] [FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜] (f : F) (a : A) :
@[simp]
theorem AlgHom.toContinuousLinearMap_norm {𝕜 : Type u_1} {A : Type u_2} [] [] [] [] (φ : A →ₐ[𝕜] 𝕜) :
def WeakDual.CharacterSpace.equivAlgHom {𝕜 : Type u_1} {A : Type u_2} [] [] [] :
() (A →ₐ[𝕜] 𝕜)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem WeakDual.CharacterSpace.equivAlgHom_coe {𝕜 : Type u_1} {A : Type u_2} [] [] [] (f : ()) :
(WeakDual.CharacterSpace.equivAlgHom f) = f
@[simp]
theorem WeakDual.CharacterSpace.equivAlgHom_symm_coe {𝕜 : Type u_1} {A : Type u_2} [] [] [] (f : A →ₐ[𝕜] 𝕜) :
(WeakDual.CharacterSpace.equivAlgHom.symm f) = f
theorem SpectrumRestricts.spectralRadius_eq {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} {A : Type u_5} [] [] [] [] [] [NormedAlgebra 𝕜₁ 𝕜₂] [IsScalarTower 𝕜₁ 𝕜₂ A] {f : 𝕜₂𝕜₁} {a : A} (h : ) :
=

If 𝕜₁ is a normed field contained as subfield of a larger normed field 𝕜₂, and if a : A is an element whose 𝕜₂ spectrum restricts to 𝕜₁, then the spectral radii over each scalar field coincide.

theorem SpectrumRestricts.nnreal_iff {A : Type u_3} [Ring A] [] {a : A} :
x, 0 x
theorem SpectrumRestricts.nnreal_of_nonneg {A : Type u_4} [Ring A] [] [] [] {a : A} (ha : 0 a) :
theorem SpectrumRestricts.real_iff {A : Type u_3} [Ring A] [] {a : A} :
x, x = x.re
theorem SpectrumRestricts.nnreal_iff_spectralRadius_le {A : Type u_3} [Ring A] [] {a : A} {t : NNReal} (ht : t) :
spectralRadius (() t - a) t