Continuous linear maps on a Hilbert space are a StarOrderedRing #
In this file we show that the continuous linear maps on a complex Hilbert space form a
StarOrderedRing. Note that they are already equipped with the Loewner partial order. We also
prove that, with respect to this partial order, a map is positive if every element of the
real spectrum is nonnegative. Consequently, when H is a Hilbert space, then H →L[ℂ] H is
equipped with all the usual instances of the continuous functional calculus.
theorem
ContinuousLinearMap.IsPositive.spectrumRestricts
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
[CompleteSpace H]
[Algebra ℝ (H →L[𝕜] H)]
[IsScalarTower ℝ 𝕜 (H →L[𝕜] H)]
{f : H →L[𝕜] H}
(hf : f.IsPositive)
:
instance
ContinuousLinearMap.instNonnegSpectrumClassRealId
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
[CompleteSpace H]
[Algebra ℝ (H →L[𝕜] H)]
[IsScalarTower ℝ 𝕜 (H →L[𝕜] H)]
:
NonnegSpectrumClass ℝ (H →L[𝕜] H)
theorem
ContinuousLinearMap.instStarOrderedRingRCLike
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
[CompleteSpace H]
[Algebra ℝ (H →L[𝕜] H)]
[IsScalarTower ℝ 𝕜 (H →L[𝕜] H)]
[ContinuousFunctionalCalculus ℝ IsSelfAdjoint]
:
StarOrderedRing (H →L[𝕜] H)
Because this takes ContinuousFunctionalCalculus ℝ IsSelfAdjoint as an argument, and for
the moment we only have this for 𝕜 := ℂ, this is not registered as an instance.
instance
ContinuousLinearMap.instStarOrderedRing
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[CompleteSpace H]
:
StarOrderedRing (H →L[ℂ] H)