Composed twirling from two commutator estimates

Stated in a bipartite model (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.unitaryTwirl_comp {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {J : Type u_5} [Fintype I] [Fintype J] (μ : I → ℝ) (ν : J → ℝ) (U : I → 𝒜) (V : J → 𝒜) (M : 𝒜) : unitaryTwirl ν V (unitaryTwirl μ U M) = unitaryTwirl (fun (p : I × J) => μ p.1 * ν p.2) (fun (p : I × J) => V p.2 * U p.1) M

Successive twirls equal the twirl by the independently sampled product.

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

Two reflective twirls stay close if each commutator is small and the second has an exact mirror.