Instances of the continuous functional calculus #
Main theorems #
IsStarNormal.instContinuousFunctionalCalculus
: the continuous functional calculus for normal elements in a unital C⋆-algebra overℂ
.IsSelfAdjoint.instContinuousFunctionalCalculus
: the continuous functional calculus for selfadjoint elements in aℂ
-algebra with a continuous functional calculus for normal elements and where every element has compact spectrum. In particular, this includes unital C⋆-algebras overℂ
.Nonneg.instContinuousFunctionalCalculus
: the continuous functional calculus for nonnegative elements in anℝ
-algebra with a continuous functional calculus for selfadjoint elements, where every element has compact spectrum, and where nonnegative elements have nonnegative spectrum. In particular, this includes unital C⋆-algebras overℝ
.CstarRing.instNonnegSpectrumClass
: In a unital C⋆-algebra overℂ
which is also aStarOrderedRing
, the spectrum of a nonnegative element is nonnegative.
Tags #
continuous functional calculus, normal, selfadjoint
instance
IsStarNormal.cfc_map
{R : Type u_1}
{A : Type u_2}
{p : A → Prop}
[CommSemiring R]
[StarRing R]
[MetricSpace R]
[TopologicalSemiring R]
[ContinuousStar R]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra R A]
[ContinuousFunctionalCalculus R p]
(a : A)
(f : R → R)
:
IsStarNormal (cfc f a)
Equations
- ⋯ = ⋯
instance
IsStarNormal.instContinuousFunctionalCalculus
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
:
ContinuousFunctionalCalculus ℂ IsStarNormal
Equations
- ⋯ = ⋯
theorem
isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{a : A}
:
An element in a C⋆-algebra is selfadjoint if and only if it is normal and its spectrum is
contained in ℝ
.
theorem
IsSelfAdjoint.spectrumRestricts
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{a : A}
(ha : IsSelfAdjoint a)
:
theorem
SpectrumRestricts.isSelfAdjoint
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
(a : A)
(ha : SpectrumRestricts a ⇑Complex.reCLM)
[IsStarNormal a]
:
A normal element whose ℂ
-spectrum is contained in ℝ
is selfadjoint.
instance
IsSelfAdjoint.instContinuousFunctionalCalculus
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
[∀ (x : A), CompactSpace ↑(spectrum ℂ x)]
:
ContinuousFunctionalCalculus ℝ IsSelfAdjoint
Equations
- ⋯ = ⋯
theorem
unitary_iff_isStarNormal_and_spectrum_subset_circle
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{u : A}
:
theorem
mem_unitary_of_spectrum_subset_circle
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{u : A}
[IsStarNormal u]
(hu : spectrum ℂ u ⊆ ↑circle)
:
theorem
CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts
{A : Type u_1}
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra ℝ A]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
{a : A}
(ha₁ : IsSelfAdjoint a)
(ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal)
:
∃ (x : A), IsSelfAdjoint x ∧ SpectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x ^ 2 = a
theorem
nonneg_iff_isSelfAdjoint_and_spectrumRestricts
{A : Type u_1}
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[TopologicalSpace A]
[Algebra ℝ A]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
:
instance
Nonneg.instContinuousFunctionalCalculus
{A : Type u_1}
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[TopologicalSpace A]
[Algebra ℝ A]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
[∀ (a : A), CompactSpace ↑(spectrum ℝ a)]
:
ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x
Equations
- ⋯ = ⋯
theorem
SpectrumRestricts.nnreal_iff_nnnorm
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
{a : A}
{t : NNReal}
(ha : IsSelfAdjoint a)
(ht : ‖a‖₊ ≤ t)
:
SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t
theorem
SpectrumRestricts.nnreal_add
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
{a : A}
{b : A}
(ha₁ : IsSelfAdjoint a)
(hb₁ : IsSelfAdjoint b)
(ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal)
(hb₂ : SpectrumRestricts b ⇑ContinuousMap.realToNNReal)
:
theorem
IsSelfAdjoint.sq_spectrumRestricts
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
{a : A}
(ha : IsSelfAdjoint a)
:
theorem
SpectrumRestricts.eq_zero_of_neg
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
{a : A}
(ha : IsSelfAdjoint a)
(ha₁ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal)
(ha₂ : SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal)
:
a = 0
theorem
SpectrumRestricts.smul_of_nonneg
{A : Type u_2}
[Ring A]
[Algebra ℝ A]
{a : A}
(ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal)
{r : ℝ}
(hr : 0 ≤ r)
:
theorem
spectrum_star_mul_self_nonneg
{A : Type u_1}
[NormedRing A]
[StarRing A]
[CstarRing A]
[CompleteSpace A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
{b : A}
(x : ℝ)
:
instance
CstarRing.instNonnegSpectrumClass
{A : Type u_1}
[NormedRing A]
[CompleteSpace A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[CstarRing A]
[NormedAlgebra ℂ A]
[StarModule ℂ A]
:
Equations
- ⋯ = ⋯
theorem
cfcHom_real_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[UniqueContinuousFunctionalCalculus ℝ A]
[UniqueContinuousFunctionalCalculus ℂ A]
{a : A}
(ha : IsSelfAdjoint a)
:
cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
theorem
cfc_real_eq_complex
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[UniqueContinuousFunctionalCalculus ℝ A]
[UniqueContinuousFunctionalCalculus ℂ A]
{a : A}
(f : ℝ → ℝ)
(ha : autoParam (IsSelfAdjoint a) _auto✝)
:
theorem
cfcHom_nnreal_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Algebra ℝ A]
[TopologicalRing A]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x]
[UniqueContinuousFunctionalCalculus ℝ A]
[NonnegSpectrumClass ℝ A]
{a : A}
(ha : 0 ≤ a)
:
cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
theorem
cfc_nnreal_eq_real
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Algebra ℝ A]
[TopologicalRing A]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
[ContinuousFunctionalCalculus NNReal fun (x : A) => 0 ≤ x]
[UniqueContinuousFunctionalCalculus ℝ A]
[NonnegSpectrumClass ℝ A]
{a : A}
(f : NNReal → NNReal)
(ha : autoParam (0 ≤ a) _auto✝)
:
cfc f a = cfc (fun (x : ℝ) => ↑(f (Real.toNNReal x))) a