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 #
A continuous linear endomorphism
T of a Hilbert space is positive if it is self adjoint
∀ x, 0 ≤ re ⟪T x, x⟫.