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} [] [] [] [NormedAlgebra š E] [] (u : ā„()) :
spectrum š āu ā
theorem spectrum.subset_circle_of_unitary {š : Type u_1} [NormedField š] {E : Type u_2} [] [] [] [NormedAlgebra š E] [] {u : E} (h : u ā ) :
spectrum š u ā
theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {A : Type u_1} [] [] [] [] [] {a : A} (ha : ) :
= ā
theorem IsStarNormal.spectralRadius_eq_nnnorm {A : Type u_1} [] [] [] [] [] (a : A) [] :
= ā
theorem IsSelfAdjoint.mem_spectrum_eq_re {A : Type u_1} [] [] [] [] [] [] {a : A} (ha : ) {z : ā} (hz : z ā ) :
z = āz.re

Any element of the spectrum of a selfadjoint is real.

theorem selfAdjoint.mem_spectrum_eq_re {A : Type u_1} [] [] [] [] [] [] (a : ā„()) {z : ā} (hz : z ā spectrum ā āa) :
z = āz.re

Any element of the spectrum of a selfadjoint is real.

theorem IsSelfAdjoint.val_re_map_spectrum {A : Type u_1} [] [] [] [] [] [] {a : A} (ha : ) :

The spectrum of a selfadjoint is real

theorem selfAdjoint.val_re_map_spectrum {A : Type u_1} [] [] [] [] [] [] (a : ā„()) :
spectrum ā āa =

The spectrum of a selfadjoint is real

theorem StarAlgHom.nnnorm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [FunLike F A B] [] [] (Ļ : F) (a : A) :

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} [] [] [] [] [] [] [] [] [] [] [FunLike F A B] [] [] (Ļ : F) (a : A) :

A star algebra homomorphism of complex Cā-algebras is norm contractive.

@[instance 100]
noncomputable instance StarAlgHom.instContinuousLinearMapClassComplex {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [FunLike F A B] [] [] :

Star algebra homomorphisms between Cā-algebras are continuous linear maps. See note [lower instance priority]

Equations
• āÆ = āÆ
theorem StarAlgEquiv.nnnorm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [EquivLike F A B] [] [] (Ļ : F) (a : A) :
theorem StarAlgEquiv.norm_map {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [EquivLike F A B] [] [] (Ļ : F) (a : A) :
theorem StarAlgEquiv.isometry {F : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [] [] [] [] [] [] [] [] [EquivLike F A B] [] [] (Ļ : F) :
Isometry āĻ
@[instance 100]
noncomputable instance WeakDual.Complex.instStarHomClass {F : Type u_1} {A : Type u_2} [] [] [] [] [] [] [] [hF : ] :

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

Equations
• āÆ = āÆ
theorem AlgHomClass.instStarAlgHomClass {F : Type u_1} {A : Type u_2} [] [] [] [] [] [] [] [hF : ] :

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

noncomputable instance WeakDual.CharacterSpace.instStarAlgHomClass {A : Type u_2} [] [] [] [] [] [] :
Equations
• āÆ = āÆ