Orthonormalization in von Neumann algebras without abelian projections

De la Salle's Theorem 1.2 (blueprint thm:orthonormalization) for a von Neumann algebra M with no nonzero abelian projection and a faithful tracial vector functional, against any state given by a summable family of vectors — in particular a vector state — with no factor hypothesis. This is the orthonormalization tier the C6b port uses (the II₁ tier of planning/mipco-track.md, Phase 6).

The vendored II₁-factor theorem (Orthogonalization.povm_orthogonalization_II₁Factor, MvN/II1Factor.lean) uses its factor hypothesis only to build the scalar centre-valued trace x ↦ τ(x) • 1; its proof reads the centre-valued trace only through IsCenterValuedTrace, and the state only through positivity, φ 1 = 1 and its trace-class form, never through normality. So the same proof, with the centre-valued trace of CenterComparison.lean in place of the scalar one, gives the theorem for every M without abelian projections (povm_orthogonalization_of_isCenterValuedTrace), and for a vector state (povm_orthogonalization_vecTrace).

theorem MIPRE.Orthonormalization.povm_orthogonalization_of_isCenterValuedTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hII : ∀ (r : H →L[ℂ] H), Orthogonalization.MvN.IsAbelianProj M r → r = 0) {E : (H →L[ℂ] H) →ₗ[ℂ] H →L[ℂ] H} (hE : Orthogonalization.MvN.IsCenterValuedTrace M 1 E) (φ : (H →L[ℂ] H) →ₗ[ℂ] ℂ) (hφ0 : ∀ x ∈ M, 0 ≤ φ (star x * x)) (hφ1 : φ 1 = 1) (hφg : ∃ (g : ℕ → H), (Summable fun (k : ℕ) => ‖g k‖ ^ 2) ∧ ∀ x ∈ M, φ x = ∑' (k : ℕ), inner ℂ (g k) (x (g k))) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : Orthogonalization.IsPOVM M a) (ε : ℝ) (hε : 1 - ε < (φ (∑ i : ι, a i * a i)).re) : ∃ (p : ι → H →L[ℂ] H), Orthogonalization.IsPVM M p ∧ (φ (∑ i : ι, star (a i - p i) * (a i - p i))).re < 9 * ε

Theorem 1.2 from a centre-valued trace: in a von Neumann algebra with no nonzero abelian projection and a centre-valued trace, a POVM that is ε-nearly projective against a positive normalized functional of trace-class form is 9ε-close to a projective measurement of the algebra.

theorem MIPRE.Orthonormalization.povm_orthogonalization_vecTrace {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (M : VonNeumannAlgebra H) (hII : ∀ (r : H →L[ℂ] H), Orthogonalization.MvN.IsAbelianProj M r → r = 0) {d : ℕ} (g : Fin d → H) (htr : ∀ x ∈ M, ∀ y ∈ M, (vecFunctional g) (x * y) = (vecFunctional g) (y * x)) (hsep : ∀ x ∈ M, (∀ (k : Fin d), x (g k) = 0) → x = 0) (ψ : H) (hψ : ‖ψ‖ = 1) {ι : Type u_1} [Fintype ι] (a : ι → H →L[ℂ] H) (ha : Orthogonalization.IsPOVM M a) (ε : ℝ) (hε : 1 - ε < ∑ i : ι, ‖(a i) ψ‖ ^ 2) : ∃ (p : ι → H →L[ℂ] H), Orthogonalization.IsPVM M p ∧ ∑ i : ι, ‖(a i - p i) ψ‖ ^ 2 < 9 * ε

Theorem 1.2 in a von Neumann algebra without abelian projections, at a vector state: for M with no nonzero abelian projection and a faithful tracial vector functional of finitely many vectors, a POVM (aᵢ) of M with ∑ᵢ ‖aᵢ ψ‖² > 1 - ε at a unit vector ψ is within ∑ᵢ ‖(aᵢ - pᵢ) ψ‖² < 9ε of a projective measurement (pᵢ) of M.