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 symmetric and ∀ x, 0 ≤ re ⟪T x, x⟫.
• ContinuousLinearMap.IsPositive : a continuous linear map is positive if it is symmetric 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][bourbaki1987]

Tags

Positive operator

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

A linear operator T on a Hilbert space is positive if it is symmetric and ∀ x, 0 ≤ re ⟪T x, x⟫.

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

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

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

theorem LinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℂ 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)

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

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

theorem LinearMap.isPositive_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →ₗ[𝕜] E) : T.IsPositive ↔ T.IsSymmetric ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LinearMap.isPositive_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : id.IsPositive

@[simp]

theorem LinearMap.isPositive_natCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} : (↑n).IsPositive

@[simp]

theorem LinearMap.isPositive_ofNat {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [n.AtLeastTwo] : (OfNat.ofNat n).IsPositive

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

theorem LinearMap.isPositive_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {T : ι → E →ₗ[𝕜] E} (s : Finset ι) (hT : ∀ i ∈ s, (T i).IsPositive) : (∑ i ∈ s, T i).IsPositive

theorem LinearMap.IsPositive.ne_zero_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) : T ≠ 0 ↔ ∃ (x : E), 0 < inner 𝕜 (T x) x

theorem LinearMap.IsPositive.smul_of_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) {c : 𝕜} (hc : 0 ≤ c) : (c • T).IsPositive

theorem LinearMap.IsPositive.isPositive_smul_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsPositive) (hT' : T ≠ 0) {α : 𝕜} : (α • T).IsPositive ↔ 0 ≤ α

theorem LinearMap.IsPositive.nonneg_eigenvalues {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsPositive) (hn : Module.finrank 𝕜 E = n) (i : Fin n) : 0 ≤ ⋯.eigenvalues hn i

instance LinearMap.instLoewnerPartialOrder {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 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).

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

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

theorem LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : IsIdempotentElem T) : T.IsPositive ↔ T.IsSymmetric

An idempotent linear map is positive iff it is symmetric.

theorem LinearMap.isPositive_linearIsometryEquiv_conj_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] {T : E →ₗ[𝕜] E} (f : E ≃ₗᵢ[𝕜] F) : (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsPositive ↔ T.IsPositive

@[simp]

theorem Matrix.isPositive_toEuclideanLin_iff {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_4} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} : (toEuclideanLin A).IsPositive ↔ A.PosSemidef

A.toEuclideanLin is positive if and only if A is positive semi-definite.

@[simp]

theorem LinearMap.posSemidef_toMatrix_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {A : E →ₗ[𝕜] E} (b : OrthonormalBasis ι 𝕜 E) : ((toMatrix b.toBasis b.toBasis) A).PosSemidef ↔ A.IsPositive

A.toMatrix is positive semi-definite if and only if A is positive.

theorem LinearMap.IsSymmetricProjection.isPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive

A symmetric projection is positive.

@[deprecated LinearMap.IsSymmetricProjection.isPositive (since := "2025-10-17")]

theorem LinearMap.IsPositive.of_isSymmetricProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive

Alias of LinearMap.IsSymmetricProjection.isPositive.

---

A symmetric projection is positive.

@[deprecated LinearMap.IsSymmetricProjection.isPositive (since := "2025-08-19")]

theorem LinearMap.IsPositive.of_isStarProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) : p.IsPositive

A star projection operator is positive.

theorem LinearMap.IsSymmetricProjection.le_iff_range_le_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {p q : E →ₗ[𝕜] E} (hp : p.IsSymmetricProjection) (hq : q.IsSymmetricProjection) : p ≤ q ↔ p.range ≤ q.range

def ContinuousLinearMap.IsPositive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : Prop

A continuous linear endomorphism T of a Hilbert space is positive if it is symmetric and ∀ x, 0 ≤ re ⟪T x, x⟫.

theorem ContinuousLinearMap.isPositive_def {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} : T.IsPositive ↔ (↑T).IsSymmetric ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x

theorem ContinuousLinearMap.isPositive_def' {𝕜 : 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 ≤ T.reApplyInnerSelf x

In a complete space, a continuous linear endomorphism T is positive if it is symmetric and ∀ x, 0 ≤ re ⟪T x, x⟫.

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

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

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

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

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

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

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

Alias of the reverse direction of ContinuousLinearMap.isPositive_toLinearMap_iff.

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

theorem ContinuousLinearMap.isPositive_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : T.IsPositive ↔ (↑T).IsSymmetric ∧ ∀ (x : E), 0 ≤ inner 𝕜 (T x) x

An operator is positive iff it is symmetric and 0 ≤ ⟪T x, x⟫.

For the version with IsSelfAdjoint instead of IsSymmetric, see ContinuousLinearMap.isPositive_iff'.

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

An operator is positive iff it is self-adjoint and 0 ≤ ⟪T x, x⟫.

For the version with IsSymmetric instead of IsSelfAdjoint, see ContinuousLinearMap.isPositive_iff.

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

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

@[simp]

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

@[simp]

theorem ContinuousLinearMap.isPositive_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : (ContinuousLinearMap.id 𝕜 E).IsPositive

@[simp]

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

@[simp]

theorem ContinuousLinearMap.isPositive_natCast {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} : (↑n).IsPositive

@[simp]

theorem ContinuousLinearMap.isPositive_ofNat {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [n.AtLeastTwo] : (OfNat.ofNat n).IsPositive

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

theorem ContinuousLinearMap.isPositive_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {T : ι → E →L[𝕜] E} (s : Finset ι) (hT : ∀ i ∈ s, (T i).IsPositive) : (∑ i ∈ s, T i).IsPositive

theorem ContinuousLinearMap.IsPositive.smul_of_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : T.IsPositive) {c : 𝕜} (hc : 0 ≤ c) : (c • T).IsPositive

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

theorem ContinuousLinearMap.isPositive_self_comp_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] (S : E →L[𝕜] F) : (S.comp (adjoint S)).IsPositive

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

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

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

theorem LinearMap.isPositive_self_comp_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] (S : E →ₗ[𝕜] F) : (S ∘ₗ adjoint S).IsPositive

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

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

theorem ContinuousLinearMap.IsPositive.conj_starProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U : Submodule 𝕜 E) {T : E →L[𝕜] E} (hT : T.IsPositive) [U.HasOrthogonalProjection] : (U.starProjection.comp (T.comp U.starProjection)).IsPositive

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

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

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

theorem ContinuousLinearMap.isPositive_iff_complex {E' : Type u_4} [NormedAddCommGroup E'] [InnerProductSpace ℂ 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)

instance ContinuousLinearMap.instLoewnerPartialOrder {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 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.

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

theorem ContinuousLinearMap.coe_le_coe_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (f g : E →L[𝕜] E) : ↑f ≤ ↑g ↔ f ≤ g

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

theorem ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : p.IsPositive ↔ IsSelfAdjoint p

An idempotent operator is positive if and only if it is self-adjoint.

theorem ContinuousLinearMap.IsPositive.of_isStarProjection {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsStarProjection p) : p.IsPositive

A star projection operator is positive.

The proof of this will soon be simplified to IsStarProjection.nonneg when we have StarOrderedRing (E →L[𝕜] E).

theorem ContinuousLinearMap.IsIdempotentElem.TFAE {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE

For an idempotent operator p, TFAE:

• (range p)ᗮ = ker p
• p is normal
• p is self-adjoint
• p is positive

theorem Submodule.starProjection_le_starProjection_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection ≤ V.starProjection ↔ U ≤ V

U.starProjection ≤ V.starProjection iff U ≤ V.

theorem Submodule.starProjection_inj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : U.starProjection = V.starProjection ↔ U = V

U.starProjection = V.starProjection iff U = V.

theorem LinearMap.IsPositive.toLinearMap_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E ≃ₗ[𝕜] E} (hT : (↑T).IsPositive) : (↑T.symm).IsPositive

@[simp]

theorem LinearEquiv.isPositive_symm_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E ≃ₗ[𝕜] E} : (↑T.symm).IsPositive ↔ (↑T).IsPositive

@[simp]

theorem InnerProductSpace.isPositive_rankOne_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) : (((rankOne 𝕜) x) x).IsPositive

theorem ContinuousLinearMap.isPositive_iff_eq_sum_rankOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {T : E →L[𝕜] E} : T.IsPositive ↔ ∃ (m : ℕ) (u : Fin m → E), T = ∑ i : Fin m, ((InnerProductSpace.rankOne 𝕜) (u i)) (u i)

In finite-dimensional spaces, a continuous linear map is positive iff it is equal to the sum of rank-one positive operators.

theorem Matrix.posSemidef_iff_eq_sum_vecMulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_4} [Finite n] {M : Matrix n n 𝕜} : M.PosSemidef ↔ ∃ (m : ℕ) (v : Fin m → n → 𝕜), M = ∑ i : Fin m, vecMulVec (v i) (star (v i))