mathlib documentation

analysis.inner_product_space.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 continuous_linear_map.is_positive {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space 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
theorem continuous_linear_map.is_positive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {T : E →L[𝕜] E} (hT : T.is_positive) (x : E) :
theorem continuous_linear_map.is_positive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {T : E →L[𝕜] E} (hT : T.is_positive) (x : E) :
theorem continuous_linear_map.is_positive.add {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [complete_space E] {T S : E →L[𝕜] E} (hT : T.is_positive) (hS : S.is_positive) :
theorem continuous_linear_map.is_positive.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [complete_space E] [complete_space F] {T : E →L[𝕜] E} (hT : T.is_positive) (S : E →L[𝕜] F) :
theorem continuous_linear_map.is_positive.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [complete_space E] [complete_space F] {T : E →L[𝕜] E} (hT : T.is_positive) (S : F →L[𝕜] E) :