mathlib3 documentation


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 #

Main statements #

References #

Tags #

Positive operator

def continuous_linear_map.is_positive {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space 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⟫.

theorem continuous_linear_map.is_positive.add {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [complete_space E] {T S : E →L[𝕜] E} (hT : T.is_positive) (hS : S.is_positive) :