mathlib3documentation

analysis.inner_product_space.positive

Positive operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

Main statements #

• continuous_linear_map.is_positive.conj_adjoint : if T : E →L[𝕜] E is positive, then for any S : E →L[𝕜] F, S ∘L T ∘L S† is also positive.
• continuous_linear_map.is_positive_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

Tags #

Positive operator

def continuous_linear_map.is_positive {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ 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.is_self_adjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {T : E →L[𝕜] E} (hT : T.is_positive) :
theorem continuous_linear_map.is_positive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ 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 𝕜] [ E] {T : E →L[𝕜] E} (hT : T.is_positive) (x : E) :
theorem continuous_linear_map.is_positive_zero {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E]  :
theorem continuous_linear_map.is_positive_one {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E]  :
theorem continuous_linear_map.is_positive.add {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ F] {T : E →L[𝕜] E} (hT : T.is_positive) (S : F →L[𝕜] E) :
theorem continuous_linear_map.is_positive.conj_orthogonal_projection {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (U : E) {T : E →L[𝕜] E} (hT : T.is_positive)  :
theorem continuous_linear_map.is_positive.orthogonal_projection_comp {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] {T : E →L[𝕜] E} (hT : T.is_positive) (U : E)  :