mathlib documentation

analysis.normed_space.star.spectrum

Spectral properties in C⋆-algebras #

In this file, we establish various propreties related to the spectrum of elements in C⋆-algebras.

theorem unitary.spectrum_subset_circle {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [complete_space E] [nontrivial E] (u : (unitary E)) :
theorem spectrum.subset_circle_of_unitary {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [complete_space E] [nontrivial E] {u : E} (h : u unitary E) :
theorem is_self_adjoint.mem_spectrum_eq_re {A : Type u_1} [normed_ring A] [normed_algebra A] [complete_space A] [star_ring A] [cstar_ring A] [star_module A] [nontrivial A] {a : A} (ha : is_self_adjoint a) {z : } (hz : z spectrum a) :
z = (z.re)

Any element of the spectrum of a selfadjoint is real.

theorem self_adjoint.mem_spectrum_eq_re {A : Type u_1} [normed_ring A] [normed_algebra A] [complete_space A] [star_ring A] [cstar_ring A] [star_module A] [nontrivial A] (a : (self_adjoint 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

The spectrum of a selfadjoint is real

theorem star_alg_hom.nnnorm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [normed_ring A] [normed_algebra A] [norm_one_class A] [complete_space A] [star_ring A] [cstar_ring A] [normed_ring B] [normed_algebra B] [norm_one_class B] [complete_space B] [star_ring B] [cstar_ring B] [hF : star_alg_hom_class F A B] (φ : F) (a : A) :

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

theorem star_alg_hom.norm_apply_le {F : Type u_1} {A : Type u_2} {B : Type u_3} [normed_ring A] [normed_algebra A] [norm_one_class A] [complete_space A] [star_ring A] [cstar_ring A] [normed_ring B] [normed_algebra B] [norm_one_class B] [complete_space B] [star_ring B] [cstar_ring B] [hF : star_alg_hom_class F A B] (φ : F) (a : A) :

A star algebra homomorphism of complex C⋆-algebras is norm contractive.

@[protected, instance]

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

Equations
@[protected, instance]
noncomputable def weak_dual.complex.star_hom_class {F : Type u_1} {A : Type u_2} [normed_ring A] [normed_algebra A] [nontrivial A] [complete_space A] [star_ring A] [cstar_ring A] [star_module A] [hF : alg_hom_class F A ] :

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

Equations
noncomputable def alg_hom_class.star_alg_hom_class {F : Type u_1} {A : Type u_2} [normed_ring A] [normed_algebra A] [nontrivial A] [complete_space A] [star_ring A] [cstar_ring A] [star_module A] [hF : alg_hom_class F A ] :

This is not an instance to avoid type class inference loops. See weak_dual.complex.star_hom_class.

Equations