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: ifT : E →L[𝕜] Eis positive, then for anyS : 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 allxsuffices to prove thatTis positive
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) :
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
- T.is_positive = (is_self_adjoint T ∧ ∀ (x : E), 0 ≤ T.re_apply_inner_self x)
theorem
continuous_linear_map.is_positive.is_self_adjoint
{𝕜 : 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}
(hT : T.is_positive) :
theorem
continuous_linear_map.is_positive.inner_nonneg_left
{𝕜 : 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}
(hT : T.is_positive)
(x : E) :
0 ≤ ⇑is_R_or_C.re (has_inner.inner (⇑T x) x)
theorem
continuous_linear_map.is_positive.inner_nonneg_right
{𝕜 : 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}
(hT : T.is_positive)
(x : E) :
0 ≤ ⇑is_R_or_C.re (has_inner.inner x (⇑T x))
theorem
continuous_linear_map.is_positive_zero
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E] :
theorem
continuous_linear_map.is_positive_one
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E] :
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) :
(T + 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 𝕜]
[normed_add_comm_group E]
[normed_add_comm_group F]
[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) :
(S.comp (T.comp (⇑continuous_linear_map.adjoint S))).is_positive
theorem
continuous_linear_map.is_positive.adjoint_conj
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[normed_add_comm_group F]
[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) :
((⇑continuous_linear_map.adjoint S).comp (T.comp S)).is_positive
theorem
continuous_linear_map.is_positive.conj_orthogonal_projection
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
[complete_space E]
(U : submodule 𝕜 E)
{T : E →L[𝕜] E}
(hT : T.is_positive)
[complete_space ↥U] :
(U.subtypeL.comp ((orthogonal_projection U).comp (T.comp (U.subtypeL.comp (orthogonal_projection U))))).is_positive
theorem
continuous_linear_map.is_positive.orthogonal_projection_comp
{𝕜 : 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}
(hT : T.is_positive)
(U : submodule 𝕜 E)
[complete_space ↥U] :
((orthogonal_projection U).comp (T.comp U.subtypeL)).is_positive
theorem
continuous_linear_map.is_positive_iff_complex
{E' : Type u_4}
[normed_add_comm_group E']
[inner_product_space ℂ E']
[complete_space E']
(T : E' →L[ℂ] E') :
T.is_positive ↔ ∀ (x : E'), ↑(⇑is_R_or_C.re (has_inner.inner (⇑T x) x)) = has_inner.inner (⇑T x) x ∧ 0 ≤ ⇑is_R_or_C.re (has_inner.inner (⇑T x) x)