Documentation

Mathlib.Analysis.InnerProductSpace.Positive

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 #

Main statements #

References #

Tags #

Positive operator

def ContinuousLinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [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
Instances For
    theorem ContinuousLinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (x : E) :
    0 IsROrC.re T x, x⟫_𝕜
    theorem ContinuousLinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : ContinuousLinearMap.IsPositive T) (x : E) :
    0 IsROrC.re x, T x⟫_𝕜
    theorem ContinuousLinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace E'] [CompleteSpace E'] (T : E' →L[] E') :
    ContinuousLinearMap.IsPositive T ∀ (x : E'), (IsROrC.re T x, x⟫_) = T x, x⟫_ 0 IsROrC.re T x, x⟫_