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} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : Prop

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

Equations

• ContinuousLinearMap.IsPositive T = (IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ ContinuousLinearMap.reApplyInnerSelf T x)

theorem ContinuousLinearMap.IsPositive.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) : IsSelfAdjoint T

theorem ContinuousLinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (x : E) : 0 ≤ RCLike.re ⟪T x, x⟫_𝕜

theorem ContinuousLinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (x : E) : 0 ≤ RCLike.re ⟪x, T x⟫_𝕜

theorem ContinuousLinearMap.isPositive_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : ContinuousLinearMap.IsPositive 0

theorem ContinuousLinearMap.isPositive_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : ContinuousLinearMap.IsPositive 1

theorem ContinuousLinearMap.IsPositive.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} {S : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (hS : ContinuousLinearMap.IsPositive S) : ContinuousLinearMap.IsPositive (T + S)

theorem ContinuousLinearMap.IsPositive.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (S : E →L[𝕜] F) : ContinuousLinearMap.IsPositive (ContinuousLinearMap.comp S (ContinuousLinearMap.comp T (ContinuousLinearMap.adjoint S)))

theorem ContinuousLinearMap.IsPositive.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (S : F →L[𝕜] E) : ContinuousLinearMap.IsPositive (ContinuousLinearMap.comp (ContinuousLinearMap.adjoint S) (ContinuousLinearMap.comp T S))

theorem ContinuousLinearMap.IsPositive.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) [CompleteSpace ↥U] : ContinuousLinearMap.IsPositive (ContinuousLinearMap.comp (Submodule.subtypeL U) (ContinuousLinearMap.comp (orthogonalProjection U) (ContinuousLinearMap.comp T (ContinuousLinearMap.comp (Submodule.subtypeL U) (orthogonalProjection U)))))

theorem ContinuousLinearMap.IsPositive.orthogonalProjection_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (U : Submodule 𝕜 E) [CompleteSpace ↥U] : ContinuousLinearMap.IsPositive (ContinuousLinearMap.comp (orthogonalProjection U) (ContinuousLinearMap.comp T (Submodule.subtypeL U)))

theorem ContinuousLinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [CompleteSpace E'] (T : E' →L[ℂ] E') : ContinuousLinearMap.IsPositive T ↔ ∀ (x : E'), ↑(RCLike.re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ RCLike.re ⟪T x, x⟫_ℂ