structure Orthogonalization.MvNStructureTheory : Prop

The structure-theory interface (PLAN.md §9.2). All fields quantify over every complex Hilbert space H : Type u and every von Neumann algebra on it.

• normal_traceClass {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) : (∀ x ∈ M, 0 ≤ φ (star x * x)) → MvN.IsNormalOn M φ → ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))

  H0 (Kadison–Ringrose 7.1.12, Takesaki III.2.14): a positive functional normal on M is, on M, of the trace-class form ∑ₖ ⟪gₖ, · gₖ⟫ with ∑ ‖gₖ‖² < ∞.

• type_decomposition {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) : ∃ (z : H →L[ℂ] H), Blocks.IsCentralProj M z ∧ MvN.IsSemifiniteAt M z ∧ MvN.IsTypeIIIAt M (1 - z)

  H1 (Takesaki V.1.19): M = z M ⊕ (1 − z) M with z M semifinite and (1 − z) M of type III.

• finite_decomposition {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) : MvN.IsFiniteProj M p → ∃ (c : H →L[ℂ] H), IsStarProjection c ∧ MvN.IsCentralIn M p c ∧ MvN.IsTypeIAt M c ∧ MvN.IsTypeII₁At M (p - c)

  H1' (Takesaki V.1.19, V.1.27): a finite algebra p M p splits along a projection c of its center Z(p M p) into a type I part c M c and a type II₁ part (p − c) M (p − c).

• semifinite_net {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Blocks.IsCentralProj M z → MvN.IsSemifiniteAt M z → ∃ (κ : Type u) (x : Preorder κ) (_ : IsDirected κ fun (x1 x2 : κ) => x1 ≤ x2) (_ : Nonempty κ) (p : κ → H →L[ℂ] H), Monotone p ∧ (∀ (α : κ), MvN.IsFiniteProj M (p α) ∧ p α * z = p α) ∧ CommutingRepetition.VN.TendstoStrongBdd Filter.atTop p z

  H2 (Takesaki V.1.37): a semifinite z M z has an increasing net of finite projections converging strongly to z.

• center_valued_trace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p : H →L[ℂ] H) : MvN.IsFiniteProj M p → ∃ (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H), MvN.IsCenterValuedTrace M p E

  H3 (Takesaki V.2.6; Anantharaman–Popa 9.1.8): every finite algebra p M p carries a center-valued trace detecting equivalence of projections.

• halving {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (z : H →L[ℂ] H) : Blocks.IsCentralProj M z → MvN.IsTypeIIIAt M z → ∀ (q : H →L[ℂ] H), IsStarProjection q → q ∈ M → q * z = q → q ≠ 0 → ∃ (e : H →L[ℂ] H), IsStarProjection e ∧ e ∈ M ∧ e * q = e ∧ MvN.MvNEquiv M e (q - e) ∧ MvN.MvNEquiv M e q

  H4 (Takesaki V.1.36): in a type III algebra every nonzero projection q splits as e + (q − e) with e ∼ q − e ∼ q.

• selection_typeI {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (p c : H →L[ℂ] H) : MvN.IsFiniteProj M p → IsStarProjection c → MvN.IsCentralIn M p c → MvN.IsTypeIAt M c → ∀ (E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H), MvN.IsCenterValuedTrace M p E → ∀ (n : ℕ) (a : Fin n → H →L[ℂ] H), (∀ (i : Fin n), a i ∈ M) → (∀ (i : Fin n), 0 ≤ a i) → ∑ i : Fin n, a i = c → ∀ (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ), (∀ x ∈ M, 0 ≤ φ (star x * x)) → MvN.IsNormalOn M φ → ∃ (q : Fin n → H →L[ℂ] H), (∀ (i : Fin n), IsStarProjection (q i) ∧ q i ∈ M ∧ q i * c = q i ∧ Commute (q i) (a i)) ∧ ∑ i : Fin n, E (q i) = c ∧ (φ (∑ i : Fin n, a i * a i)).re ≤ (φ (∑ i : Fin n, q i * a i)).re

  H5 (the paper's Lemma 3.1 for finite type I algebras — the direct sum over d of the algebras M_d(ℂ) ⊗ L∞(Ω_d), proved there by measurable selection): for the type I part c M c (c a central projection of p M p) of a finite algebra p M p with center-valued trace E, a POVM (aᵢ) of c M c and a functional φ positive and normal on M, there are projections qᵢ ≤ c of M commuting with aᵢ, with ∑ E(qᵢ) = c and φ(∑ qᵢ aᵢ) ≥ φ(∑ aᵢ²) (the intermediate inequality of the paper's proof, DIFFERENCES.md D6 addendum).

• polar {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (x : H →L[ℂ] H) : x ∈ M → ∃ u ∈ M, star u * u = MvN.rightSupport x ∧ u * star u = MvN.leftSupport x ∧ x = u * CFC.sqrt (star x * x)

  H6 (Anantharaman–Popa 2.2.4): polar decomposition inside M, with the partial isometry between the right and left supports.