Combining approximate commutations across a bipartite state

Transfer the second unitary to the other party, commute the first, and transfer back. The POVM square-sum bound controls both transfer errors without an alphabet factor.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the four-link argument for a state model, with the family in front a column contraction (StateModel.IsColContraction); the bipartite version with the mirror of Alice's V on the second player's side, where it commutes with everything of the first player's.

theorem MIPRE.Introspection.commutator_product_bound {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {A : Type u_2} [Fintype A] (M : A → 𝒞) (hM : Ψ.IsColContraction M) (U V W : 𝒞) (hU : star U * U = 1) (hW : star W * W = 1) (hWU : W * U = U * W) (hWM : ∀ (a : A), W * M a = M a * W) : ∑ a : A, Ψ.snorm (M a * (U * V) - U * V * M a) ^ 2 ≤ 4 * ∑ a : A, Ψ.snorm (M a * U - U * M a) ^ 2 + 4 * ∑ a : A, Ψ.snorm (M a * V - V * M a) ^ 2 + 8 * Ψ.snorm (V - W) ^ 2

The four-link commutation argument, with an arbitrary commuting mirror W.

theorem MIPRE.Introspection.two_sided_commutation {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} [Fintype A] (M : POVMIn A 𝒜) (U V : 𝒜) (W : ℬ) (hU : star U * U = 1) (hW : star W * W = 1) : ∑ a : A, Ψ.stateSqNorm (M.op a * (U * V) - U * V * M.op a) ≤ 4 * ∑ a : A, Ψ.stateSqNorm (M.op a * U - U * M.op a) + 4 * ∑ a : A, Ψ.stateSqNorm (M.op a * V - V * M.op a) + 8 * Ψ.xSqNorm V W

The bipartite version: W is the second party's mirror of Alice's V.

theorem MIPRE.Introspection.two_sided_commutation_avg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_4} [Fintype A] {X : Type u_5} {I : Type u_6} {J : Type u_7} [Fintype X] [Fintype I] [Fintype J] (D : X → ℝ) (hD : ∀ (x : X), 0 ≤ D x) (μ : X → I → ℝ) (ν : X → J → ℝ) (hμ0 : ∀ (x : X) (i : I), 0 ≤ μ x i) (hν0 : ∀ (x : X) (j : J), 0 ≤ ν x j) (hμ1 : ∀ (x : X), ∑ i : I, μ x i = 1) (hν1 : ∀ (x : X), ∑ j : J, ν x j = 1) (M : X → POVMIn A 𝒜) (U : X → I → 𝒜) (V : X → J → 𝒜) (W : X → J → ℬ) (hU : ∀ (x : X) (i : I), star (U x i) * U x i = 1) (hW : ∀ (x : X) (j : J), star (W x j) * W x j = 1) : ∑ x : X, D x * ∑ i : I, μ x i * ∑ j : J, ν x j * ∑ a : A, Ψ.stateSqNorm ((M x).op a * (U x i * V x j) - U x i * V x j * (M x).op a) ≤ 4 * ∑ x : X, D x * ∑ i : I, μ x i * ∑ a : A, Ψ.stateSqNorm ((M x).op a * U x i - U x i * (M x).op a) + 4 * ∑ x : X, D x * ∑ j : J, ν x j * ∑ a : A, Ψ.stateSqNorm ((M x).op a * V x j - V x j * (M x).op a) + 8 * ∑ x : X, D x * ∑ j : J, ν x j * Ψ.xSqNorm (V x j) (W x j)

Independent conditional unitary distributions preserve the same explicit constants.