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) : SpectrumRestricts f ⇑ContinuousMap.realToNNReal

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 ℝ (H →L[𝕜] H) IsSelfAdjoint] : StarOrderedRing (H →L[𝕜] H)

Because this takes ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) 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)