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)) :
spectrum 𝕜 ↑u ⊆ metric.sphere 0 1
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) :
spectrum 𝕜 u ⊆ metric.sphere 0 1
theorem
spectral_radius_eq_nnnorm_of_self_adjoint
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[norm_one_class A]
{a : A}
(ha : a ∈ self_adjoint A) :
theorem
spectral_radius_eq_nnnorm_of_star_normal
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[norm_one_class A]
(a : A)
[is_star_normal a] :
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 : A}
(ha : a ∈ self_adjoint A)
{z : ℂ}
(hz : z ∈ spectrum ℂ a) :
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) :
Any element of the spectrum of a selfadjoint is real.
theorem
self_adjoint.coe_re_map_spectrum
{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 : a ∈ self_adjoint A) :
The spectrum of a selfadjoint is real
theorem
self_adjoint.coe_re_map_spectrum'
{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)) :
The spectrum of a selfadjoint is real