Products of commuting positive operators

theorem Orthogonalization.mul_nonneg_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : Commute x y) : 0 ≤ x * y

The product of two commuting positive operators is positive. (Without the commutation hypothesis this is false.) This is Mathlib's Commute.mul_nonneg, restated with the hypotheses in the order in which the proof uses them.

theorem Orthogonalization.sq_le_self_of_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x : H →L[ℂ] H} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : x * x ≤ x

If 0 ≤ x ≤ 1 then x² ≤ x: indeed x - x² = x (1 - x) is a product of commuting positive operators.

theorem Orthogonalization.one_sub_sq_le_one_sub_sq' {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {s : H →L[ℂ] H} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) : (1 - s) * (1 - s) ≤ 1 - s * s

If 0 ≤ s ≤ 1 then (1 - s)² ≤ 1 - s², because (1 - s²) - (1 - s)² = 2 (s - s²) = 2 s (1 - s) ≥ 0. This is the operator inequality used in the assembly step of the paper.

theorem Orthogonalization.le_of_nonneg_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (h : 0 ≤ y - x) : x ≤ y

A convenience restatement of sub_nonneg: an operator inequality is the positivity of the difference.

theorem Orthogonalization.nonneg_sub_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (h : x ≤ y) : 0 ≤ y - x

A convenience restatement of sub_nonneg in the other direction.

theorem Orthogonalization.conj_le_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (h : x ≤ y) (c : H →L[ℂ] H) : star c * x * c ≤ star c * y * c

Conjugation by a fixed operator is monotone for the Loewner order.

theorem Orthogonalization.conj_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x : H →L[ℂ] H} (hx : 0 ≤ x) (c : H →L[ℂ] H) : 0 ≤ star c * x * c

Conjugation by a fixed operator preserves positivity.

Compression by a commuting projection

theorem Orthogonalization.IsStarProjection.mul_nonneg_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {q b : H →L[ℂ] H} (hq : IsStarProjection q) (hb : 0 ≤ b) (h : Commute q b) : 0 ≤ q * b

If q is a projection commuting with a positive b, then q b is positive.

theorem Orthogonalization.IsStarProjection.mul_le_of_commute {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {q b : H →L[ℂ] H} (hq : IsStarProjection q) (hb : 0 ≤ b) (h : Commute q b) : q * b ≤ b

If q is a projection commuting with a positive b, then q b ≤ b, because b - q b = (1 - q) b is a product of commuting positive operators.

The continuous functional calculus square root

theorem Orthogonalization.sqrt_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (y : H →L[ℂ] H) : 0 ≤ CFC.sqrt y

The square root of an operator is positive (junk value 0 if the argument is not positive). Re-export of CFC.sqrt_nonneg.

theorem Orthogonalization.sqrt_mul_sqrt_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {y : H →L[ℂ] H} (hy : 0 ≤ y) : CFC.sqrt y * CFC.sqrt y = y

√y √y = y for 0 ≤ y. Re-export of CFC.sqrt_mul_sqrt_self.

theorem Orthogonalization.sqrt_le_one_of_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {y : H →L[ℂ] H} (hy1 : y ≤ 1) : CFC.sqrt y ≤ 1

If y ≤ 1 then √y ≤ 1, by operator monotonicity of the square root and √1 = 1. (Positivity of y is not needed: if y is not positive then √y = 0 ≤ 1.)

theorem Orthogonalization.Commute.sqrt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (h : Commute x y) : Commute x (CFC.sqrt y)

Anything commuting with y commutes with √y: the square root is a continuous functional calculus of y. (Positivity of y is not needed because of the junk value.)

theorem Orthogonalization.Commute.sqrt_left {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {x y : H →L[ℂ] H} (h : Commute x y) : Commute (CFC.sqrt x) y

Commute.sqrt with the arguments in the other order.

Positive linear functionals

A positive linear functional on H →L[ℂ] H is a ℂ-linear map φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ with 0 ≤ φ (star x * x) for every x, the order on ℂ being the ComplexOrder one (0 ≤ z ↔ 0 ≤ z.re ∧ z.im = 0). We do not bundle the hypothesis, so that the lemmas apply verbatim to the functional underlying a normal state.

theorem Orthogonalization.re_star_mul_self_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (x : H →L[ℂ] H) : 0 ≤ (φ (star x * x)).re

A positive functional takes nonnegative real values on star x * x.

theorem Orthogonalization.nonneg_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {x : H →L[ℂ] H} (hx : 0 ≤ x) : 0 ≤ φ x

A positive functional is nonnegative on positive operators: every positive operator is of the form star c * c (CStarAlgebra.nonneg_iff_eq_star_mul_self).

theorem Orthogonalization.im_eq_zero_of_nonneg {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {x : H →L[ℂ] H} (hx : 0 ≤ x) : (φ x).im = 0

A positive functional is real on positive operators.

theorem Orthogonalization.le_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {x y : H →L[ℂ] H} (hxy : x ≤ y) : φ x ≤ φ y

A positive functional is monotone (hence so is its real part).

theorem Orthogonalization.re_le_re_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) {x y : H →L[ℂ] H} (hxy : x ≤ y) : (φ x).re ≤ (φ y).re

The real part of a positive functional is monotone for the Loewner order.

def Orthogonalization.toPositiveLinearMap {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) : (H →L[ℂ] H) →ₚ[ℂ] ℂ

A positive functional as a bundled PositiveLinearMap; this is the input of Mathlib's GNS construction, which is how the Cauchy–Schwarz inequality of Orthogonalization/PhiNorm.lean is obtained.

Equations

• Orthogonalization.toPositiveLinearMap φ hφ = { toLinearMap := φ, monotone' := ⋯ }

@[simp]

theorem Orthogonalization.toPositiveLinearMap_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ} (hφ : ∀ (z : H →L[ℂ] H), 0 ≤ φ (star z * z)) (x : H →L[ℂ] H) : (toPositiveLinearMap φ hφ) x = φ x