Retaining a classical fibre after twirling

The consistency marginal lets us retain the matching block of a nearby measurement. An exactly consistent projective mirror moves the rightmost projector to the front, where it is a contraction. No outcome-count factor enters the estimate.

Stated for a state model (Phase 4 of planning/mipco-track.md).

theorem MIPRE.Introspection.snorm_right_projector_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) (P R E : 𝒞) (hRsa : star R = R) (hRid : R * R = R) (hPR : (Ψ.π P) Ψ.ψ = (Ψ.π R) Ψ.ψ) (hER : E * R = R * E) : Ψ.snorm (E * P) ^ 2 ≤ Ψ.snorm E ^ 2

Multiplication on the right by a projector is contractive when it has a commuting mirror.

theorem MIPRE.Introspection.joint_mul_marginal {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {Y : Type u_2} {A : Type u_3} [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {M : Y × A → 𝒞} (hM : IsPVMIn M) (y : Y) (a : A) : M (y, a) * ∑ b : A, M (y, b) = M (y, a)

A joint PVM element is unchanged by multiplication by its own first marginal.

theorem MIPRE.Introspection.isColContraction_row {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {Y : Type u_2} {A : Type u_3} [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {M : Y × A → 𝒞} (hM : IsPVMIn M) (y : Y) : Ψ.IsColContraction fun (a : A) => M (y, a)

A row of a joint PVM is a column contraction.

theorem MIPRE.Introspection.retained_fibre_dist {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {Y : Type u_2} {A : Type u_3} [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] (M T : Y × A → 𝒞) (P R : Y → 𝒞) (hM : IsPVMIn M) (hR : IsPVMIn R) (hPR : ∀ (y : Y), (Ψ.π (P y)) Ψ.ψ = (Ψ.π (R y)) Ψ.ψ) (hMR : ∀ (y : Y) (a : A), M (y, a) * R y = R y * M (y, a)) (hTR : ∀ (y : Y) (a : A), T (y, a) * R y = R y * T (y, a)) : ∑ p : Y × A, Ψ.snorm (M p - T p * P p.1) ^ 2 ≤ 2 * ∑ y : Y, Ψ.snorm (∑ a : A, M (y, a) - P y) ^ 2 + 2 * ∑ p : Y × A, Ψ.snorm (M p - T p) ^ 2

Keeping the matching target fibre costs twice the marginal error plus twice the original error.