Documentation

Mathlib.Analysis.Normed.Algebra.GelfandFormula

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 #

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) :
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)โปยน.

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 spectralRadius of a is the limit of the sequence โ€–a ^ nโ€–โ‚Š ^ (1 / n).

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

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

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

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

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.

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

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
Instances For
    @[simp]