# 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)

## Equations

- ⋯ = ⋯

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)

## Equations

- ⋯ = ⋯