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

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