Small facts about projections

theorem Orthogonalization.MvN.le_of_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a b : H →L[ℂ] H} (ha : IsStarProjection a) (hb : IsStarProjection b) (h : a * b = a) : a ≤ b

A projection a with a b = a lies below the projection b in the Loewner order.

theorem Orthogonalization.MvN.le_one_of_isStarProjection {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a : H →L[ℂ] H} (ha : IsStarProjection a) : a ≤ 1

A projection is a contraction in the Loewner order.

theorem Orthogonalization.MvN.sub_mul_sub_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {a b c : H →L[ℂ] H} (ha : IsStarProjection a) (hb : IsStarProjection b) (hc : IsStarProjection c) (hab : a * b = a) (hbc : b * c = b) : (c - b) * (c - a) = c - b

For projections a ≤ b ≤ c: (c − b) (c − a) = c − b.

Partial isometries between subprojections

structure Orthogonalization.MvN.IsPartialBetween {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p q w : H →L[ℂ] H) : Prop

w ∈ M is a partial isometry with initial projection w* w ≤ p and final projection w w* ≤ q.

• mem : w ∈ M
• proj : IsStarProjection (star w * w)
• init_le : star w * w * p = star w * w
• final_le : w * star w * q = w * star w

theorem Orthogonalization.MvN.IsPartialBetween.isStarProjection_mul_star {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : IsStarProjection (w * star w)

theorem Orthogonalization.MvN.IsPartialBetween.init_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : star w * w ∈ M

theorem Orthogonalization.MvN.IsPartialBetween.final_mem {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : w * star w ∈ M

theorem Orthogonalization.MvN.IsPartialBetween.mul_init {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : w * (star w * w) = w

w (w* w) = w.

theorem Orthogonalization.MvN.IsPartialBetween.star_mul_final {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : star w * (w * star w) = star w

w* (w w*) = w*.

theorem Orthogonalization.MvN.IsPartialBetween.final_mul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : w * star w * w = w

(w w*) w = w.

theorem Orthogonalization.MvN.IsPartialBetween.mul_right_eq_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : w * p = w

w p = w.

theorem Orthogonalization.MvN.IsPartialBetween.mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w p' q' : H →L[ℂ] H} (h : IsPartialBetween M p' q' w) (hp : p' * p = p') (hq : q' * q = q') : IsPartialBetween M p q w

Enlarging the target projections.

theorem Orthogonalization.MvN.IsPartialBetween.norm_le_one {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : ‖w‖ ≤ 1

Partial isometries are contractions.

theorem Orthogonalization.MvN.IsPartialBetween.init_le_loewner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) (hp : IsStarProjection p) : star w * w ≤ p

w* w ≤ p in the Loewner order.

theorem Orthogonalization.MvN.IsPartialBetween.adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) : IsPartialBetween M q p (star w)

The adjoint of a partial isometry (≤ p) → (≤ q) is a partial isometry (≤ q) → (≤ p).

theorem Orthogonalization.MvN.IsPartialBetween.mul_left_eq_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w : H →L[ℂ] H} (h : IsPartialBetween M p q w) (hq : IsSelfAdjoint q) : q * w = w

q w = w (q self-adjoint).

theorem Orthogonalization.MvN.zero_isPartialBetween {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p q : H →L[ℂ] H) : IsPartialBetween M p q 0

Orthogonal sums of partial isometries

theorem Orthogonalization.MvN.IsPartialBetween.add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q w u : H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hw : IsPartialBetween M p q w) (hu : IsPartialBetween M (p - star w * w) (q - w * star w) u) : IsPartialBetween M p q (w + u) ∧ star (w + u) * (w + u) = star w * w + star u * u ∧ (w + u) * star (w + u) = w * star w + u * star u

The sum of a partial isometry w : (≤ p) → (≤ q) and a partial isometry between the complements p − w* w, q − w w* is a partial isometry (≤ p) → (≤ q) whose initial and final projections are the sums.

The corner lemma

theorem Orthogonalization.MvN.exists_mul_mul_ne_zero_of_factor {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) {e f : H →L[ℂ] H} (he : IsStarProjection e) (heM : e ∈ M) (he0 : e ≠ 0) (hf : IsStarProjection f) (hfM : f ∈ M) (hf0 : f ≠ 0) : ∃ y ∈ M, e * y * f ≠ 0

In a factor, the corner e M f between two nonzero projections is nonzero (the central support of a nonzero projection is 1).

The extension step

theorem Orthogonalization.MvN.exists_extension_of_ne {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) (hpolar : ∀ x ∈ M, ∃ u ∈ M, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x)) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (hτf : ∀ x ∈ M, τ (star x * x) = 0 → x = 0) {p q w : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (hq : IsStarProjection q) (hqM : q ∈ M) (hw : IsPartialBetween M p q w) (hr : star w * w ≠ p) (hl : w * star w ≠ q) : ∃ (u : H →L[ℂ] H), IsPartialBetween M (p - star w * w) (q - w * star w) u ∧ 0 < (τ (star u * u)).re

If neither complement p − w* w, q − w w* vanishes, the partial isometry w extends by a nonzero partial isometry u between the complements; its initial projection has positive trace when τ is faithful.

The greedy choice

theorem Orthogonalization.MvN.exists_good_extension {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) {p q w : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (hw : IsPartialBetween M p q w) : ∃ (u : H →L[ℂ] H), IsPartialBetween M (p - star w * w) (q - w * star w) u ∧ ∀ (u' : H →L[ℂ] H), IsPartialBetween M (p - star w * w) (q - w * star w) u' → (τ (star u' * u')).re ≤ 2 * (τ (star u * u)).re

Among the partial isometries between the complements p − w* w, q − w w* there is one whose initial projection has trace at least half the supremum of the available traces.

Increasing chains of partial isometries and their strong limits

structure Orthogonalization.MvN.IsChain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p q : H →L[ℂ] H) (w u : ℕ → H →L[ℂ] H) : Prop

An increasing chain of partial isometries (≤ p) → (≤ q): w (n+1) = w n + u n with u n a partial isometry between the complements of w n.

• step (n : ℕ) : IsPartialBetween M p q (w n)
• extend (n : ℕ) : IsPartialBetween M (p - star (w n) * w n) (q - w n * star (w n)) (u n)
• succ_eq (n : ℕ) : w (n + 1) = w n + u n

theorem Orthogonalization.MvN.IsChain.adjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hc : IsChain M p q w u) : IsChain M q p (fun (n : ℕ) => star (w n)) fun (n : ℕ) => star (u n)

The adjoint chain.

theorem Orthogonalization.MvN.IsChain.init_succ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) (n : ℕ) : star (w (n + 1)) * w (n + 1) = star (w n) * w n + star (u n) * u n

theorem Orthogonalization.MvN.IsChain.final_succ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) (n : ℕ) : w (n + 1) * star (w (n + 1)) = w n * star (w n) + u n * star (u n)

theorem Orthogonalization.MvN.IsChain.init_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) : Monotone fun (n : ℕ) => star (w n) * w n

theorem Orthogonalization.MvN.IsChain.final_mono {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) : Monotone fun (n : ℕ) => w n * star (w n)

theorem Orthogonalization.MvN.IsChain.init_mul_init {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) {n m : ℕ} (h : n ≤ m) : star (w n) * w n * (star (w m) * w m) = star (w n) * w n

theorem Orthogonalization.MvN.IsChain.final_mul_final {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) {n m : ℕ} (h : n ≤ m) : w n * star (w n) * (w m * star (w m)) = w n * star (w n)

theorem Orthogonalization.MvN.IsChain.star_mul_ext {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) {n m : ℕ} (h : n ≤ m) : star (w n) * u m = 0

wₙ* uₘ = 0 for n ≤ m: the range of uₘ is orthogonal to that of wₘ, hence to that of wₙ.

theorem Orthogonalization.MvN.IsChain.star_mul_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) {n m : ℕ} (h : n ≤ m) : star (w n) * w m = star (w n) * w n

wₙ* wₘ = wₙ* wₙ for n ≤ m.

theorem Orthogonalization.MvN.IsChain.norm_sub_sq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) (ξ : H) {n m : ℕ} (h : n ≤ m) : ‖(w m) ξ - (w n) ξ‖ ^ 2 = (inner ℂ ξ ((star (w m) * w m) ξ)).re - (inner ℂ ξ ((star (w n) * w n) ξ)).re

‖wₘ ξ − wₙ ξ‖² = ⟪ξ, (wₘ* wₘ − wₙ* wₙ) ξ⟫ for n ≤ m.

theorem Orthogonalization.MvN.IsChain.cauchySeq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) (ξ : H) : CauchySeq fun (n : ℕ) => (w n) ξ

The orbits wₙ ξ are Cauchy.

theorem Orthogonalization.MvN.IsChain.exists_limit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M : VonNeumannAlgebra H} {p q : H →L[ℂ] H} {w u : ℕ → H →L[ℂ] H} (hp : IsStarProjection p) (hq : IsStarProjection q) (hc : IsChain M p q w u) : ∃ W ∈ M, (∀ (ξ : H), Filter.Tendsto (fun (n : ℕ) => (w n) ξ) Filter.atTop (nhds (W ξ))) ∧ IsStarProjection (star W * W) ∧ star W * W * p = star W * W ∧ ∀ (n : ℕ), star (w n) * w n * (star W * W) = star (w n) * w n

The strong limit of an increasing chain of partial isometries: an operator W ∈ M whose initial projection W* W is a projection below p dominating every wₙ* wₙ (it is the strong limit of the increasing sequence wₙ* wₙ).

theorem Orthogonalization.MvN.eq_star_of_tendsto {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {T : ℕ → H →L[ℂ] H} {S V : H →L[ℂ] H} (hS : ∀ (ξ : H), Filter.Tendsto (fun (n : ℕ) => (T n) ξ) Filter.atTop (nhds (S ξ))) (hV : ∀ (ξ : H), Filter.Tendsto (fun (n : ℕ) => (star (T n)) ξ) Filter.atTop (nhds (V ξ))) : V = star S

If Tₙ → S and Tₙ* → V strongly, then V = S*.

The comparison theorem

theorem Orthogonalization.MvN.mvNEquiv_of_trace_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hfactor : ∀ z ∈ M, (∀ y ∈ M, Commute z y) → ∃ (c : ℂ), z = c • 1) (τ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hτ0 : ∀ x ∈ M, 0 ≤ τ (star x * x)) (hτtr : ∀ x ∈ M, ∀ y ∈ M, τ (x * y) = τ (y * x)) (hτf : ∀ x ∈ M, τ (star x * x) = 0 → x = 0) (hpolar : ∀ x ∈ M, ∃ u ∈ M, star u * u = rightSupport x ∧ u * star u = leftSupport x ∧ x = u * CFC.sqrt (star x * x)) {p q : H →L[ℂ] H} (hp : IsStarProjection p) (hpM : p ∈ M) (hq : IsStarProjection q) (hqM : q ∈ M) (h : τ p = τ q) : MvNEquiv M p q

Comparison of projections in a factor with a faithful tracial positive functional (Anantharaman–Popa 9.1.8): τ(p) = τ(q) implies p ∼ q. hpolar is the polar decomposition inside M (interface field H6).