# Positive operators #

In this file we define positive operators in a Hilbert space. We follow Bourbaki's choice of requiring self adjointness in the definition.

## Main definitions #

• IsPositive : a continuous linear map is positive if it is self adjoint and ∀ x, 0 ≤ re ⟪T x, x⟫

## Main statements #

• ContinuousLinearMap.IsPositive.conj_adjoint : if T : E →L[𝕜] E is positive, then for any S : E →L[𝕜] F, S ∘L T ∘L S† is also positive.
• ContinuousLinearMap.isPositive_iff_complex : in a complex Hilbert space, checking that ⟪T x, x⟫ is a nonnegative real number for all x suffices to prove that T is positive

## References #

• [Bourbaki, Topological Vector Spaces][bourbaki1987]

## Tags #

Positive operator

def ContinuousLinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [] [] [] (T : E →L[𝕜] E) :

A continuous linear endomorphism T of a Hilbert space is positive if it is self adjoint and ∀ x, 0 ≤ re ⟪T x, x⟫.

Equations
• T.IsPositive = ( ∀ (x : E), 0 T.reApplyInnerSelf x)
Instances For
theorem ContinuousLinearMap.IsPositive.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) :
theorem ContinuousLinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :
0 RCLike.re T x, x⟫_𝕜
theorem ContinuousLinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :
0 RCLike.re x, T x⟫_𝕜
theorem ContinuousLinearMap.isPositive_zero {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
theorem ContinuousLinearMap.isPositive_one {𝕜 : Type u_1} {E : Type u_2} [] [] [] :
theorem ContinuousLinearMap.IsPositive.add {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} {S : E →L[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :
(T + S).IsPositive
theorem ContinuousLinearMap.IsPositive.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) (S : E →L[𝕜] F) :
theorem ContinuousLinearMap.IsPositive.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) (S : F →L[𝕜] E) :
theorem ContinuousLinearMap.IsPositive.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [] [] [] (U : ) {T : E →L[𝕜] E} (hT : T.IsPositive) [] :
(U.subtypeL.comp (.comp (T.comp (U.subtypeL.comp )))).IsPositive
theorem ContinuousLinearMap.IsPositive.orthogonalProjection_comp {𝕜 : Type u_1} {E : Type u_2} [] [] [] {T : E →L[𝕜] E} (hT : T.IsPositive) (U : ) [] :
(.comp (T.comp U.subtypeL)).IsPositive
theorem ContinuousLinearMap.isPositive_iff_complex {E' : Type u_4} [] [] [] (T : E' →L[] E') :
T.IsPositive ∀ (x : E'), (RCLike.re T x, x⟫_) = T x, x⟫_ 0 RCLike.re T x, x⟫_
instance ContinuousLinearMap.instLoewnerPartialOrder {𝕜 : Type u_1} {E : Type u_2} [] [] [] :

The (Loewner) partial order on continuous linear maps on a Hilbert space determined by f ≤ g if and only if g - f is a positive linear map (in the sense of ContinuousLinearMap.IsPositive). With this partial order, the continuous linear maps form a StarOrderedRing.

Equations
• ContinuousLinearMap.instLoewnerPartialOrder =
theorem ContinuousLinearMap.le_def {𝕜 : Type u_1} {E : Type u_2} [] [] [] (f : E →L[𝕜] E) (g : E →L[𝕜] E) :
f g (g - f).IsPositive
theorem ContinuousLinearMap.nonneg_iff_isPositive {𝕜 : Type u_1} {E : Type u_2} [] [] [] (f : E →L[𝕜] E) :
0 f f.IsPositive