Documentation

Mathlib.Analysis.NormedSpace.Star.Spectrum

Spectral properties in Cā‹†-algebras #

In this file, we establish various properties related to the spectrum of elements in Cā‹†-algebras.

theorem unitary.spectrum_subset_circle {š•œ : Type u_1} [NormedField š•œ] {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra š•œ E] [CompleteSpace E] (u : { x // x āˆˆ unitary E }) :
spectrum š•œ ā†‘u āŠ† Metric.sphere 0 1
theorem spectrum.subset_circle_of_unitary {š•œ : Type u_1} [NormedField š•œ] {E : Type u_2} [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra š•œ E] [CompleteSpace E] {u : E} (h : u āˆˆ unitary E) :
theorem IsSelfAdjoint.mem_spectrum_eq_re {A : Type u_1} [NormedRing A] [NormedAlgebra ā„‚ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ā„‚ A] {a : A} (ha : IsSelfAdjoint a) {z : ā„‚} (hz : z āˆˆ spectrum ā„‚ a) :
z = ā†‘z.re

Any element of the spectrum of a selfadjoint is real.

theorem selfAdjoint.mem_spectrum_eq_re {A : Type u_1} [NormedRing A] [NormedAlgebra ā„‚ A] [CompleteSpace A] [StarRing A] [CstarRing A] [StarModule ā„‚ A] (a : { x // x āˆˆ selfAdjoint A }) {z : ā„‚} (hz : z āˆˆ spectrum ā„‚ ā†‘a) :
z = ā†‘z.re

Any element of the spectrum of a selfadjoint is real.

The spectrum of a selfadjoint is real

A star algebra homomorphism of complex Cā‹†-algebras is norm contractive.

theorem StarAlgHom.norm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [NormedRing A] [NormedAlgebra ā„‚ A] [CompleteSpace A] [StarRing A] [CstarRing A] [NormedRing B] [NormedAlgebra ā„‚ B] [CompleteSpace B] [StarRing B] [CstarRing B] [hF : StarAlgHomClass F ā„‚ A B] (Ļ† : F) (a : A) :

A star algebra homomorphism of complex Cā‹†-algebras is norm contractive.

This instance is provided instead of StarAlgHomClass to avoid type class inference loops. See note [lower instance priority]

This is not an instance to avoid type class inference loops. See WeakDual.Complex.instStarHomClass.

Instances For