Approximate commutation controls twirling in the state-dependent norm

This is the paper's lem:mixing-U, with constant one and all outcome sums explicit. The state need not be invariant under any of the unitaries.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md), for unitaries and operators of the first player's algebra. The unitaries are unitary on both sides: in infinite dimension an isometry U* U = 1 need not have U U* = 1, which the matrix proof took from finite dimension.

theorem MIPRE.Introspection.stateSqNorm_mul_of_isometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (U M : 𝒜) (hU : star U * U = 1) : Ψ.stateSqNorm (U * M) = Ψ.stateSqNorm M

Left multiplication by an isometry preserves the state-dependent squared norm.

def MIPRE.Introspection.unitaryTwirl {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} [Fintype I] (μ : I → ℝ) (U : I → 𝒜) (M : 𝒜) : 𝒜

Twirling against a finitely supported probability distribution.

Equations

• MIPRE.Introspection.unitaryTwirl μ U M = ∑ u : I, ↑(μ u) • (U u * M * star (U u))

theorem MIPRE.Introspection.unitaryTwirl_dist_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] (μ : I → ℝ) (hμ0 : ∀ (u : I), 0 ≤ μ u) (hμ1 : ∑ u : I, μ u = 1) (U : I → 𝒜) (hU : ∀ (u : I), star (U u) * U u = 1) (hU' : ∀ (u : I), U u * star (U u) = 1) (M : 𝒜) : Ψ.stateSqNorm (unitaryTwirl μ U M - M) ≤ ∑ u : I, μ u * Ψ.stateSqNorm (M * star (U u) - star (U u) * M)

Jensen and left-unitary invariance bound the twirl error by the commutator error.

theorem MIPRE.Introspection.unitaryTwirl_outcome_dist_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} [Fintype I] {X : Type u_5} {A : Type u_6} [Fintype X] [Fintype A] (D : X → ℝ) (hD : ∀ (x : X), 0 ≤ D x) (μ : X → I → ℝ) (hμ0 : ∀ (x : X) (u : I), 0 ≤ μ x u) (hμ1 : ∀ (x : X), ∑ u : I, μ x u = 1) (U : X → I → 𝒜) (hU : ∀ (x : X) (u : I), star (U x u) * U x u = 1) (hU' : ∀ (x : X) (u : I), U x u * star (U x u) = 1) (M : X → A → 𝒜) : ∑ x : X, D x * ∑ a : A, Ψ.stateSqNorm (unitaryTwirl (μ x) (U x) (M x a) - M x a) ≤ ∑ x : X, D x * ∑ u : I, μ x u * ∑ a : A, Ψ.stateSqNorm (M x a * star (U x u) - star (U x u) * M x a)

The outcome-summed, question-averaged form, with no alphabet or dimension loss.