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
: ifT : E →L[𝕜] E
is positive, then for anyS : 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 allx
suffices to prove thatT
is positive
References #
Tags #
Positive operator
def
ContinuousLinearMap.IsPositive
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
(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 = (IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x)
Instances For
theorem
ContinuousLinearMap.IsPositive.isSelfAdjoint
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
{T : E →L[𝕜] E}
(hT : T.IsPositive)
:
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 : T.IsPositive)
(x : E)
:
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 : T.IsPositive)
(x : E)
:
theorem
ContinuousLinearMap.isPositive_zero
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
:
theorem
ContinuousLinearMap.isPositive_one
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
:
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 : T.IsPositive)
(hS : S.IsPositive)
:
(T + S).IsPositive
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 : T.IsPositive)
(S : E →L[𝕜] F)
:
(S.comp (T.comp (ContinuousLinearMap.adjoint S))).IsPositive
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 : T.IsPositive)
(S : F →L[𝕜] E)
:
((ContinuousLinearMap.adjoint S).comp (T.comp S)).IsPositive
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 : T.IsPositive)
[CompleteSpace ↥U]
:
(U.subtypeL.comp ((orthogonalProjection U).comp (T.comp (U.subtypeL.comp (orthogonalProjection U))))).IsPositive
theorem
ContinuousLinearMap.IsPositive.orthogonalProjection_comp
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
{T : E →L[𝕜] E}
(hT : T.IsPositive)
(U : Submodule 𝕜 E)
[CompleteSpace ↥U]
:
((orthogonalProjection U).comp (T.comp U.subtypeL)).IsPositive
theorem
ContinuousLinearMap.isPositive_iff_complex
{E' : Type u_4}
[NormedAddCommGroup E']
[InnerProductSpace ℂ E']
[CompleteSpace E']
(T : E' →L[ℂ] E')
:
instance
ContinuousLinearMap.instLoewnerPartialOrder
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
:
PartialOrder (E →L[𝕜] E)
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 = PartialOrder.mk ⋯
theorem
ContinuousLinearMap.le_def
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
(f : E →L[𝕜] E)
(g : E →L[𝕜] E)
:
theorem
ContinuousLinearMap.nonneg_iff_isPositive
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[CompleteSpace E]
(f : E →L[𝕜] E)
: