Gelfand's formula and other results on the spectrum in complex Banach algebras

This file contains results on the spectrum of elements in a complex Banach algebra, including Gelfand's formula and the Gelfand-Mazur theorem and the fact that every element in a complex Banach algebra has nonempty spectrum.

Main results

• 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.
• 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

Implementation notes

Note that it is important here that the complex analysis files are privately imported, since the material proven here gets used in contexts that have nothing to do with complex analysis (i.e. C⋆-algebras, etc).

theorem spectrum.hasDerivAt_resolvent {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a) : HasDerivAt (resolvent a) (-resolvent a k ^ 2) k

theorem spectrum.differentiableOn_inverse_one_sub_smul {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] {a : A} {r : NNReal} (hr : ↑r < (spectralRadius 𝕜 a)⁻¹) : DifferentiableOn 𝕜 (fun (z : 𝕜) => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)

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} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.limsup (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a

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} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.Tendsto (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))

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.gelfand_formula {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.Tendsto (fun (n : ℕ) => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))

Alias of spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius.

---

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} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] (a : A) : Filter.Tendsto (fun (n : ℕ) => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) Filter.atTop (nhds (spectralRadius ℂ a))

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} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) : (spectrum ℂ a).Nonempty

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

theorem spectrum.exists_nnnorm_eq_spectralRadius {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) : ∃ z ∈ spectrum ℂ a, ↑‖z‖₊ = spectralRadius ℂ a

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} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) {r : NNReal} (hr : ∀ z ∈ spectrum ℂ a, ‖z‖₊ < r) : spectralRadius ℂ 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.

theorem spectrum.map_polynomial_aeval {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (p : Polynomial ℂ) : spectrum ℂ ((Polynomial.aeval a) p) = (fun (k : ℂ) => Polynomial.eval k p) '' spectrum ℂ a

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

theorem spectrum.map_pow {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A] (a : A) (n : ℕ) : spectrum ℂ (a ^ n) = (fun (x : ℂ) => x ^ n) '' spectrum ℂ a

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} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) {a : A} {z : ℂ} (h : z ∈ spectrum ℂ a) : (algebraMap ℂ A) z = a

noncomputable def NormedRing.algEquivComplexOfComplete {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] : ℂ ≃ₐ[ℂ] A

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

• NormedRing.algEquivComplexOfComplete hA = { toFun := ⇑(algebraMap ℂ A), invFun := fun (a : A) => ⋯.some, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem NormedRing.algEquivComplexOfComplete_apply {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] (a : ℂ) : (algEquivComplexOfComplete hA) a = (algebraMap ℂ A) a

@[simp]

theorem NormedRing.algEquivComplexOfComplete_symm_apply {A : Type u_2} [NormedRing A] [NormedAlgebra ℂ A] (hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0) [CompleteSpace A] (a : A) : (algEquivComplexOfComplete hA).symm a = ⋯.some