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

Murray–von Neumann equivalence p ∼ q of two projections of M: a partial isometry v ∈ M with v* v = p and v v* = q (Section 2, "we say that two projections p, q ∈ M are equivalent … if there is u ∈ M such that u* u = p, u u* = q").

Equations

• Orthogonalization.MvN.MvNEquiv M p q = ∃ v ∈ M, star v * v = p ∧ v * star v = q

def Orthogonalization.MvN.IsFiniteProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) : Prop

A finite projection of M: a projection of M with no proper equivalent subprojection (q ≤ p, q ∼ p ⇒ q = p; Takesaki V.1.16, equivalent to the paper's "p M p is finite", Section 2).

Equations

• Orthogonalization.MvN.IsFiniteProj M p = (IsStarProjection p ∧ p ∈ M ∧ ∀ (q : H →L[ℂ] H), IsStarProjection q → q ∈ M → q * p = q → Orthogonalization.MvN.MvNEquiv M q p → q = p)

def Orthogonalization.MvN.IsAbelianProj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) : Prop

An abelian projection of M: a projection p ∈ M such that p M p is commutative (Section 2, in the definition of type II₁).

Equations

• Orthogonalization.MvN.IsAbelianProj M p = (IsStarProjection p ∧ p ∈ M ∧ ∀ x ∈ M, ∀ y ∈ M, p * x * p * (p * y * p) = p * y * p * (p * x * p))

def Orthogonalization.MvN.IsSemifiniteAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

z M z is semifinite: every nonzero projection of M below z majorizes a nonzero finite projection (Section 2; projection-wise form, DIFFERENCES.md D7). The notion is intrinsic to the corner z M z (finiteness of q ≤ z in M and in z M z agree), so it applies to z central in M or in a corner p M p.

Equations

• One or more equations did not get rendered due to their size.

def Orthogonalization.MvN.IsTypeIIIAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

z M z is of type III: it contains no nonzero finite projection (Section 2; intrinsic to the corner z M z).

Equations

• Orthogonalization.MvN.IsTypeIIIAt M z = ∀ (p : H →L[ℂ] H), Orthogonalization.MvN.IsFiniteProj M p → p * z = p → p = 0

def Orthogonalization.MvN.IsTypeIAt {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

z M z is of type I: every nonzero projection of M below z majorizes a nonzero abelian projection (Takesaki V.1.17, "discrete", in the equivalent projection-wise form, DIFFERENCES.md D7; intrinsic to the corner z M z).

Equations

• Orthogonalization.MvN.IsTypeIAt M z = ∀ (p : H →L[ℂ] H), IsStarProjection p → p ∈ M → p * z = p → p ≠ 0 → ∃ (q : H →L[ℂ] H), Orthogonalization.MvN.IsAbelianProj M q ∧ q ≠ 0 ∧ q * p = q

def Orthogonalization.MvN.IsTypeII₁At {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Prop

z M z is of type II₁: z is finite and z M z contains no nonzero abelian projection (Section 2: "finite and 0 is the only projection p such that p M p is commutative"; intrinsic to the corner z M z).

Equations

• Orthogonalization.MvN.IsTypeII₁At M z = (Orthogonalization.MvN.IsFiniteProj M z ∧ ∀ (p : H →L[ℂ] H), Orthogonalization.MvN.IsAbelianProj M p → p * z = p → p = 0)

The matrix algebra M_n(M) on H^n

The paper's Lemma 3.2 and the type III case work in M_n(M); we realize it as the von Neumann algebra of operators on H^n = BlockSpace H (Fin n) commuting with the amplification y ⊕ ⋯ ⊕ y of every y ∈ M' (its elements are exactly the block matrices with entries in M'' = M).

noncomputable def Orthogonalization.MvN.amplify {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (n : ℕ) (x : H →L[ℂ] H) : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)

The amplification x ↦ x ⊕ ⋯ ⊕ x (n copies) on H^n.

Equations

• Orthogonalization.MvN.amplify n x = Orthogonalization.FinDim.blockProj fun (x_1 : Fin n) => x

noncomputable def Orthogonalization.MvN.entry {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {n : ℕ} (X : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) (i j : Fin n) : H →L[ℂ] H

The (i, j) block entry of an operator on H^n.

Equations

• Orthogonalization.MvN.entry X i j = Orthogonalization.FinDim.proj i ∘SL X ∘SL Orthogonalization.FinDim.embed j

noncomputable def Orthogonalization.MvN.matrixAlgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (n : ℕ) : VonNeumannAlgebra (FinDim.BlockSpace H (Fin n))

The matrix algebra M_n(M): the commutant, on H^n, of the amplified commutant {y ⊕ ⋯ ⊕ y | y ∈ M'} (Mathlib's StarSubalgebra.centralizer closes the set under star first; a no-op here since M' is self-adjoint).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Orthogonalization.MvN.rightSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : H →L[ℂ] H

The right support of x: the projection onto (ker x)ᗮ (the smallest projection p with x p = x; u* u in the polar decomposition, Anantharaman–Popa 2.2.4 — the paper's Lemma 3.2 calls this projection p₀, "the left support": DIFFERENCES.md D6 addendum).

Equations

• Orthogonalization.MvN.rightSupport x = (↑x).kerᗮ.starProjection

noncomputable def Orthogonalization.MvN.leftSupport {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (x : H →L[ℂ] H) : H →L[ℂ] H

The left support of x: the projection onto the closure of the range of x (the smallest projection q with q x = x; u u* in the polar decomposition).

Equations

• Orthogonalization.MvN.leftSupport x = (↑x).range.topologicalClosure.starProjection

def Orthogonalization.MvN.IsNormalOn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) : Prop

A functional is normal on M when it is continuous along bounded strongly convergent nets of elements of M with limit in M — the normal' field of NormalState, for unbundled functionals (DIFFERENCES.md D3).

Equations

• One or more equations did not get rendered due to their size.

def Orthogonalization.MvN.TendstoWeakBdd {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {κ : Type u_1} (l : Filter κ) (T : κ → H →L[ℂ] H) (L : H →L[ℂ] H) : Prop

Bounded weak-operator convergence of a net of operators: the norms are bounded and ⟪ξ, T k η⟫ → ⟪ξ, L η⟫ for all ξ, η (the weak operator topology on bounded sets, which coincides there with the σ-weak topology; Takesaki II.2.6). The weak counterpart of TendstoStrongBdd.

Equations

• Orthogonalization.MvN.TendstoWeakBdd l T L = ((∃ (C : ℝ), ∀ (k : κ), ‖T k‖ ≤ C) ∧ ∀ (ξ η : H), Filter.Tendsto (fun (k : κ) => inner ℂ ξ ((T k) η)) l (nhds (inner ℂ ξ (L η))))

def Orthogonalization.MvN.IsCentralIn {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p c : H →L[ℂ] H) : Prop

c is a central element of the corner p M p: c ∈ p M p and c commutes with every element of p M p (so c ∈ Z(p M p); for p = 1 this is c ∈ Z(M)).

Equations

• Orthogonalization.MvN.IsCentralIn M p c = (c ∈ M ∧ p * c * p = c ∧ ∀ y ∈ M, p * y * p = y → Commute c y)

structure Orthogonalization.MvN.IsCenterValuedTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H) : Prop

A center-valued trace on the finite algebra p M p (p a finite projection of M): a linear map E on B(H) which, on p M p, takes values in the center Z(p M p), is positive, tracial, the identity on Z(p M p), Z(p M p)-linear, faithful, normal (weak-operator continuous on bounded sets), detects equivalence of projections (Takesaki V.2.6; Anantharaman–Popa 9.1.8), and admits the division E b = z E r (0 ≤ z ≤ p central) for 0 ≤ b ≤ r (the functional calculus of the abelian algebra Z(p M p)). Only the values of E on p M p are constrained.

• mem_center (x : H →L[ℂ] H) : x ∈ M → p * x * p = x → IsCentralIn M p (E x)

  Values in Z(p M p).

• nonneg (x : H →L[ℂ] H) : x ∈ M → p * x * p = x → 0 ≤ x → 0 ≤ E x

  Positivity.

• trace (x : H →L[ℂ] H) : x ∈ M → p * x * p = x → ∀ y ∈ M, p * y * p = y → E (x * y) = E (y * x)

  The trace property.

• center_fixed (c : H →L[ℂ] H) : IsCentralIn M p c → E c = c

  The identity on the center Z(p M p).

• center_mul (c : H →L[ℂ] H) : IsCentralIn M p c → ∀ x ∈ M, p * x * p = x → E (c * x) = c * E x

  Z(p M p)-linearity (the conditional-expectation property).

• faithful (x : H →L[ℂ] H) : x ∈ M → p * x * p = x → E (star x * x) = 0 → x = 0

  Faithfulness.

• normal {κ : Type u} (l : Filter κ) (T : κ → H →L[ℂ] H) (L : H →L[ℂ] H) : (∀ (k : κ), T k ∈ M ∧ p * T k * p = T k) → L ∈ M → p * L * p = L → TendstoWeakBdd l T L → TendstoWeakBdd l (fun (k : κ) => E (T k)) (E L)

  Normality: continuity along bounded weak-operator convergent nets of p M p.

• equiv_of_eq (q q' : H →L[ℂ] H) : IsStarProjection q → q ∈ M → q * p = q → IsStarProjection q' → q' ∈ M → q' * p = q' → E q = E q' → MvNEquiv M q q'

  Comparison: projections of p M p with the same trace are equivalent.

• div (r : H →L[ℂ] H) : IsStarProjection r → r ∈ M → r * p = r → ∀ b ∈ M, 0 ≤ b → b ≤ r → ∃ (z : H →L[ℂ] H), IsCentralIn M p z ∧ 0 ≤ z ∧ z ≤ p ∧ E b = z * E r

  Division in the abelian algebra Z(p M p): for 0 ≤ b ≤ r with r a projection of p M p, E b = z * E r for some central 0 ≤ z ≤ p.

• equiv_of_eq_matrix (n : ℕ) (P Q : FinDim.BlockSpace H (Fin n) →L[ℂ] FinDim.BlockSpace H (Fin n)) : P ∈ matrixAlgebra M n → IsStarProjection P → P * amplify n p = P → Q ∈ matrixAlgebra M n → IsStarProjection Q → Q * amplify n p = Q → ∑ i : Fin n, E (entry P i i) = ∑ i : Fin n, E (entry Q i i) → MvNEquiv (matrixAlgebra M n) P Q

  Comparison in M_n(p M p) (Takesaki V.2.6, V.2.8 for the finite algebra M_n(p M p), whose center-valued trace is X ↦ (1/n) ∑ᵢ E(Xᵢᵢ)): projections of M_n(M) below 1_n ⊗ p with the same diagonal trace ∑ᵢ E(Xᵢᵢ) are equivalent.