Orthonormalization in a dyadic pair

The form of de la Salle's Theorem 1.2 that the orthonormalization sites of the C6b port call: in a dyadic pair (BipartiteModel.IsDyadicPair, MIPRE/Foundations/DyadicPair.lean) neither player's operators contain a nonzero abelian projection (Theorem K′ of reports/c6b-paper-proofs.md, §3), which is the hypothesis hII of povm_orthogonalization_finitePair. So a POVM of either player's algebra, nearly projective at the model's unit state, is close to a projective measurement of that algebra, with no further hypothesis (povm_orthogonalization_dyadicPair, and povm_orthogonalization_dyadicPairB for the second player, through the exchange of the players).

theorem MIPRE.Orthonormalization.povm_orthogonalization_dyadicPair {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) (hM : M.IsDyadicPair) (hψ : ‖M.ψ‖ = 1) {Λ : 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 dyadic pair (cor:orthonormalization-dyadic-pair): a POVM P of the first player's algebra of a dyadic pair with ∑ₐ ‖π(πA(Pₐ)) ψ‖² > 1 - ε at the model's unit state is within ∑ₐ ‖π(πA(Pₐ - Qₐ)) ψ‖² < 9ε of a projective measurement Q of that algebra. The first player's operators contain no nonzero abelian projection (BipartiteModel.IsDyadicPair.eq_zero_of_abelianA), so povm_orthogonalization_finitePair applies.

theorem MIPRE.Orthonormalization.povm_orthogonalization_dyadicPairB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hM : M.IsDyadicPair) (hψ : ‖M.ψ‖ = 1) {Λ : Type u_4} [Fintype Λ] (P : POVMIn Λ ℬ) (ε : ℝ) (hε : 1 - ε < ∑ b : Λ, ‖(M.π (M.πB (P.op b))) M.ψ‖ ^ 2) : ∃ (Q : Λ → ℬ), IsPVMIn Q ∧ ∑ b : Λ, ‖(M.π (M.πB (P.op b - Q b))) M.ψ‖ ^ 2 < 9 * ε

Orthonormalization in a dyadic pair, for the second player (cor:orthonormalization-dyadic-pair): a POVM P of the second player's algebra of a dyadic pair with ∑_b ‖π(πB(P_b)) ψ‖² > 1 - ε at the model's unit state is within ∑_b ‖π(πB(P_b - Q_b)) ψ‖² < 9ε of a projective measurement Q of that algebra: povm_orthogonalization_dyadicPair for the model with the players exchanged.