Positive operators #

In this file we define when an operator in a Hilbert space is positive. We follow Bourbaki's choice of requiring self adjointness in the definition.

Main definitions #

LinearMap.IsPositive : a linear map is positive if it is self adjoint and ∀ x, 0 ≤ re ⟪T x, x⟫.
ContinuousLinearMap.IsPositive : a continuous linear map is positive if it is self adjoint and ∀ x, 0 ≤ re ⟪T x, x⟫.

Main statements #

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

References #

Bourbaki, Topological Vector Spaces

Tags #

Positive operator

source

def ContinuousLinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace 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.IsPositive = (IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x)

Instances For

source

theorem ContinuousLinearMap.IsPositive.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) :

IsSelfAdjoint T

source

theorem ContinuousLinearMap.IsPositive.inner_left_eq_inner_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :

inner 𝕜 (T x) x = inner 𝕜 x (T x)

source

theorem ContinuousLinearMap.IsPositive.re_inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ RCLike.re (inner 𝕜 (T x) x)

source

theorem ContinuousLinearMap.IsPositive.re_inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ RCLike.re (inner 𝕜 x (T x))

source

theorem ContinuousLinearMap.isPositive_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) :

T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x

source

theorem ContinuousLinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ inner 𝕜 (T x) x

source

theorem ContinuousLinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ inner 𝕜 x (T x)

source

@[simp]

theorem ContinuousLinearMap.isPositive_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

IsPositive 0

source

@[simp]

theorem ContinuousLinearMap.isPositive_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

IsPositive 1

source

@[simp]

theorem ContinuousLinearMap.isPositive_natCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {n : ℕ} :

(↑n).IsPositive

source

@[simp]

theorem ContinuousLinearMap.isPositive_ofNat {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {n : ℕ} [n.AtLeastTwo] :

(OfNat.ofNat n).IsPositive

source

theorem ContinuousLinearMap.IsPositive.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T S : E →L[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :

(T + S).IsPositive

source

theorem ContinuousLinearMap.IsPositive.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : T.IsPositive) (S : E →L[𝕜] F) :

(S.comp (T.comp (adjoint S))).IsPositive

source

theorem ContinuousLinearMap.IsPositive.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] {T : E →L[𝕜] E} (hT : T.IsPositive) (S : F →L[𝕜] E) :

((adjoint S).comp (T.comp S)).IsPositive

source

theorem ContinuousLinearMap.IsPositive.conj_orthogonalProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive) [CompleteSpace ↥U] :

(U.subtypeL.comp (U.orthogonalProjection.comp (T.comp (U.subtypeL.comp U.orthogonalProjection)))).IsPositive

source

theorem ContinuousLinearMap.IsPositive.orthogonalProjection_comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsPositive) (U : Submodule 𝕜 E) [CompleteSpace ↥U] :

(U.orthogonalProjection.comp (T.comp U.subtypeL)).IsPositive

source

theorem ContinuousLinearMap.antilipschitz_of_forall_le_inner_map {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_4} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (f : H →L[𝕜] H) {c : NNReal} (hc : 0 < c) (h : ∀ (x : H), ‖x‖ ^ 2 * ↑c ≤ ‖inner 𝕜 (f x) x‖) :

AntilipschitzWith c⁻¹ ⇑f

source

theorem ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (f : E →L[𝕜] E) {c : NNReal} (hc : 0 < c) (h : ∀ (x : E), ‖x‖ ^ 2 * ↑c ≤ ‖inner 𝕜 (f x) x‖) :

IsUnit f

source

theorem ContinuousLinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [CompleteSpace E'] (T : E' →L[ℂ ] E') :

T.IsPositive ↔ ∀ (x : E'), ↑(RCLike.re (inner ℂ (T x) x)) = inner ℂ (T x) x ∧ 0 ≤ RCLike.re (inner ℂ (T x) x)

source

instance ContinuousLinearMap.instLoewnerPartialOrder {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] :

PartialOrder (E →L[𝕜] E)

The (Loewner) partial order on continuous linear maps on a Hilbert space determined by f ≤ g if and only if g - f is a positive linear map (in the sense of ContinuousLinearMap.IsPositive). With this partial order, the continuous linear maps form a StarOrderedRing.

Equations

ContinuousLinearMap.instLoewnerPartialOrder = { le := fun (f g : E →L[𝕜] E) => (g - f).IsPositive, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source

theorem ContinuousLinearMap.le_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (f g : E →L[𝕜] E) :

f ≤ g ↔ (g - f).IsPositive

source

theorem ContinuousLinearMap.nonneg_iff_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (f : E →L[𝕜] E) :

0 ≤ f ↔ f.IsPositive

source

def LinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :

Prop

A linear map T of a Hilbert space is positive if it is self adjoint and ∀ x, 0 ≤ re ⟪T x, x⟫.

Equations

T.IsPositive = (IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 (T x) x))

Instances For

source

theorem LinearMap.IsPositive.isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) :

IsSelfAdjoint T

source

theorem LinearMap.IsPositive.re_inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ RCLike.re (inner 𝕜 (T x) x)

source

theorem LinearMap.IsPositive.re_inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ RCLike.re (inner 𝕜 x (T x))

source

theorem LinearMap.isPositive_toContinuousLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] (T : E →ₗ[𝕜] E) :

(toContinuousLinearMap T).IsPositive ↔ T.IsPositive

source

theorem ContinuousLinearMap.isPositive_toLinearMap_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) :

(↑T).IsPositive ↔ T.IsPositive

source

theorem LinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] [FiniteDimensional ℂ E'] (T : E' →ₗ[ℂ ] E') :

T.IsPositive ↔ ∀ (x : E'), ↑(RCLike.re (inner ℂ (T x) x)) = inner ℂ (T x) x ∧ 0 ≤ RCLike.re (inner ℂ (T x) x)

source

theorem LinearMap.IsPositive.isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) :

T.IsSymmetric

source

theorem LinearMap.isPositive_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) :

T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x

source

theorem LinearMap.IsPositive.inner_nonneg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ inner 𝕜 (T x) x

source

theorem LinearMap.IsPositive.inner_nonneg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (x : E) :

0 ≤ inner 𝕜 x (T x)

source

@[simp]

theorem LinearMap.isPositive_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

IsPositive 0

source

@[simp]

theorem LinearMap.isPositive_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

IsPositive 1

source

@[simp]

theorem LinearMap.isPositive_natCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} :

(↑n).IsPositive

source

@[simp]

theorem LinearMap.isPositive_ofNat {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} [n.AtLeastTwo] :

(OfNat.ofNat n).IsPositive

source

theorem LinearMap.IsPositive.add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} (hT : T.IsPositive) (hS : S.IsPositive) :

(T + S).IsPositive

source

theorem LinearMap.IsPositive.conj_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (S : E →ₗ[𝕜] F) :

(S ∘ₗ T ∘ₗ adjoint S).IsPositive

source

theorem LinearMap.IsPositive.adjoint_conj {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (S : F →ₗ[𝕜] E) :

(adjoint S ∘ₗ T ∘ₗ S).IsPositive

source

instance LinearMap.instLoewnerPartialOrder {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :

PartialOrder (E →ₗ[𝕜] E)

The (Loewner) partial order on linear maps on a Hilbert space determined by f ≤ g if and only if g - f is a positive linear map (in the sense of LinearMap.IsPositive).

Equations

LinearMap.instLoewnerPartialOrder = { le := fun (f g : E →ₗ[𝕜] E) => (g - f).IsPositive, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source

theorem LinearMap.le_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f g : E →ₗ[𝕜] E) :

f ≤ g ↔ (g - f).IsPositive

source

theorem LinearMap.nonneg_iff_isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E) :

0 ≤ f ↔ f.IsPositive

Documentation

Mathlib.Analysis.InnerProductSpace.Positive

Positive operators #

Main definitions #

Main statements #

References #

Tags #