Instances of the continuous functional calculus #
Main theorems #
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ℝ.
Tags #
continuous functional calculus, normal, selfadjoint
Pull back a non-unital instance from a unital one on the unitization #
noncomputable def
cfcₙAux
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
(a : A)
(ha : p a)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
:
This is an auxiliary definition used for constructing an instance of the non-unital continuous functional calculus given a instance of the unital one on the unitization.
This is the natural non-unital star homomorphism obtained from the chain
calc
C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
_ ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
_ →⋆ₐ[𝕜] A⁺¹ := cfcHom
This range of this map is contained in the range of (↑) : A → A⁺¹ (see cfcₙAux_mem_range_inr),
and so we may restrict it to A to get the necessary homomorphism for the non-unital continuous
functional calculus.
Equations
- cfcₙAux hp₁ a ha = ((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp ContinuousMapZero.toContinuousMapHom
Instances For
theorem
cfcₙAux_id
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
(a : A)
(ha : p a)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
:
theorem
isClosedEmbedding_cfcₙAux
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
(a : A)
(ha : p a)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
:
Topology.IsClosedEmbedding ⇑(cfcₙAux ⋯ a ha)
theorem
spec_cfcₙAux
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
(a : A)
(ha : p a)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
(f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)
:
theorem
cfcₙAux_mem_range_inr
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
(a : A)
(ha : p a)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
[CompleteSpace A]
(f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜)
:
theorem
RCLike.nonUnitalContinuousFunctionalCalculus
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NonUnitalNormedRing A]
[StarRing A]
[NormedSpace 𝕜 A]
[IsScalarTower 𝕜 A A]
[SMulCommClass 𝕜 A A]
[StarModule 𝕜 A]
{p : A → Prop}
{p₁ : Unitization 𝕜 A → Prop}
(hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x)
[ContinuousFunctionalCalculus 𝕜 (Unitization 𝕜 A) p₁]
[CompleteSpace A]
[CStarRing A]
:
Continuous functional calculus for selfadjoint elements #
theorem
isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
{a : A}
:
An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in ℝ.
theorem
IsSelfAdjoint.quasispectrumRestricts
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
{a : A}
:
Alias of the forward direction of isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts.
An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in ℝ.
theorem
QuasispectrumRestricts.isSelfAdjoint
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
(a : A)
(ha : QuasispectrumRestricts a ⇑Complex.reCLM)
[IsStarNormal a]
:
A normal element whose ℂ-quasispectrum is contained in ℝ is selfadjoint.
instance
IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
:
theorem
isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ A 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 ℂ A IsStarNormal]
{a : A}
(ha : IsSelfAdjoint a)
:
theorem
SpectrumRestricts.isSelfAdjoint
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ A 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 ℂ A IsStarNormal]
:
theorem
IsSelfAdjoint.spectrum_nonempty
{A : Type u_2}
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra ℝ A]
[ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[Nontrivial A]
{a : A}
(ha : IsSelfAdjoint a)
:
Continuous functional calculus for nonnegative elements #
theorem
CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts
{A : Type u_1}
[NonUnitalRing A]
[StarRing A]
[TopologicalSpace A]
[Module ℝ A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
{a : A}
(ha₁ : IsSelfAdjoint a)
(ha₂ : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal)
:
∃ (x : A), IsSelfAdjoint x ∧ QuasispectrumRestricts x ⇑ContinuousMap.realToNNReal ∧ x * x = a
theorem
nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts
{A : Type u_1}
[NonUnitalRing A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[TopologicalSpace A]
[Module ℝ A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
:
instance
Nonneg.instNonUnitalContinuousFunctionalCalculus
{A : Type u_1}
[NonUnitalRing A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[TopologicalSpace A]
[Module ℝ A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
:
NonUnitalContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x
theorem
NNReal.spectrum_nonempty
{A : Type u_2}
[Ring A]
[StarRing A]
[LE A]
[TopologicalSpace A]
[Algebra NNReal A]
[ContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x]
[Nontrivial A]
{a : A}
(ha : 0 ≤ a)
:
theorem
CFC.exists_sqrt_of_isSelfAdjoint_of_spectrumRestricts
{A : Type u_1}
[Ring A]
[StarRing A]
[TopologicalSpace A]
[Algebra ℝ A]
[ContinuousFunctionalCalculus ℝ A 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 ℝ A 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 ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
:
ContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x
The restriction of a continuous functional calculus is equal to the original one #
theorem
cfcHom_real_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ A IsStarNormal]
[T2Space A]
{a : A}
(ha : IsSelfAdjoint a)
:
theorem
cfc_real_eq_complex
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ A IsStarNormal]
[T2Space A]
{a : A}
(f : ℝ → ℝ)
(ha : IsSelfAdjoint a := by cfc_tac)
:
theorem
cfcₙHom_real_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[T2Space A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
{a : A}
(ha : IsSelfAdjoint a)
:
theorem
cfcₙ_real_eq_complex
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[StarRing A]
[Module ℂ A]
[IsScalarTower ℂ A A]
[SMulCommClass ℂ A A]
[T2Space A]
[NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
{a : A}
(f : ℝ → ℝ)
(ha : IsSelfAdjoint a := by cfc_tac)
:
theorem
cfcHom_nnreal_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Algebra ℝ A]
[IsTopologicalRing A]
[T2Space A]
[ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
(ha : 0 ≤ a)
:
theorem
cfc_nnreal_eq_real
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Algebra ℝ A]
[IsTopologicalRing A]
[T2Space A]
[ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
(f : NNReal → NNReal)
(ha : 0 ≤ a := by cfc_tac)
:
theorem
cfcₙHom_nnreal_eq_restrict
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Module ℝ A]
[IsTopologicalRing A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[T2Space A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
(ha : 0 ≤ a)
:
theorem
cfcₙ_nnreal_eq_real
{A : Type u_1}
[TopologicalSpace A]
[NonUnitalRing A]
[PartialOrder A]
[StarRing A]
[StarOrderedRing A]
[Module ℝ A]
[IsTopologicalRing A]
[IsScalarTower ℝ A A]
[SMulCommClass ℝ A A]
[T2Space A]
[NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
[NonnegSpectrumClass ℝ A]
{a : A}
(f : NNReal → NNReal)
(ha : 0 ≤ a := by cfc_tac)
: