Orthonormalization in a finite pair without abelian projections

The form of de la Salle's Theorem 1.2 that the C6b port consumes, stated in this repository's model vocabulary so that it can be used outside MIPRE/Background/Orthonormalization/: a POVM in the first algebra of a finite pair (MIPRE/Foundations/FinitePair.lean) whose operators contain no nonzero abelian projection, nearly projective at the model's state, is close to a projective measurement of that algebra (povm_orthogonalization_finitePair). The second player's version is the same theorem for the model with the players exchanged.

The first player's operators of a finite pair are the commutant of the second player's, so they form a Mathlib VonNeumannAlgebra with no bicommutant theorem (vnA: its M″ = M field is S‴ = S′; mem_vnA_iff); the vector trace of the finite pair is a faithful tracial vector functional on it; and the model's state is a vector state. povm_orthogonalization_vecTrace then applies, and its projective measurement lies in the operators of the algebra, from which injectivity pulls it back.

noncomputable def MIPRE.Orthonormalization.vnA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : VonNeumannAlgebra M.H

The first player's von Neumann algebra of a bipartite model: the commutant of the second player's operators, as a Mathlib VonNeumannAlgebra on the model's space. Its M″ = M field is S‴ = S′, as for the vendored matrixAlgebra, so no bicommutant theorem is needed.

Equations

• MIPRE.Orthonormalization.vnA M = { toStarSubalgebra := StarSubalgebra.centralizer ℂ M.opsB, centralizer_centralizer' := ⋯ }

theorem MIPRE.Orthonormalization.mem_vnA_iff {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsFinitePair) {T : M.H →L[ℂ] M.H} : T ∈ vnA M ↔ T ∈ M.opsA

In a finite pair, the first player's von Neumann algebra is the first player's operators: an operator commuting with the second player's is one of the first player's (commutantA), and the first player's operators commute with the second player's and their adjoints.

theorem MIPRE.Orthonormalization.povm_orthogonalization_finitePair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) (hM : M.IsFinitePair) (hψ : ‖M.ψ‖ = 1) (hII : ∀ r ∈ M.opsA, IsStarProjection r → (∀ x ∈ M.opsA, ∀ y ∈ M.opsA, r * x * r * (r * y * r) = r * y * r * (r * x * r)) → r = 0) {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ 𝒜) (ε : ℝ) (hε : 1 - ε < ∑ a : Λ, ‖(M.π (M.πA (P.op a))) M.ψ‖ ^ 2) : ∃ (Q : Λ → 𝒜), IsPVMIn Q ∧ ∑ a : Λ, ‖(M.π (M.πA (P.op a - Q a))) M.ψ‖ ^ 2 < 9 * ε

Orthonormalization in a finite pair without abelian projections: if the first player's operators of a finite pair contain no nonzero abelian projection, a POVM P of the first player's algebra with ∑ₐ ‖π(πA(Pₐ)) ψ‖² > 1 - ε at the model's unit state is within ∑ₐ ‖π(πA(Pₐ - Qₐ)) ψ‖² < 9ε of a projective measurement Q of that algebra.