Completing the matching blocks of a twirled measurement

In a bipartite model whose first player's algebra carries a register, Matrix V V 𝒜 (Phase 4 of planning/mipco-track.md): a register operator P is smulKron 1 P, and a register projection P with an ancilla operator X is smulKron X P.

def MIPRE.Introspection.controlledPOVM {V : Type u_1} {Y : Type u_2} {A : Type u_3} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] [Fintype A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : Y → Matrix V V ℂ) (hP : IsPVM P) (Q : Y → POVMIn A 𝒜) : POVMIn (Y × A) (Matrix V V 𝒜)

Read a projective register, then use the POVM selected by its outcome on the ancilla.

Equations

• MIPRE.Introspection.controlledPOVM P hP Q = { mats := fun (p : Y × A) => ⟨MIPRE.smulKron ((Q p.1).op p.2) (P p.1), ⋯⟩, nonneg := ⋯, normalized := ⋯ }

theorem MIPRE.Introspection.controlledPOVM_op {V : Type u_1} {Y : Type u_2} {A : Type u_3} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : Y → Matrix V V ℂ) (hP : IsPVM P) (Q : Y → POVMIn A 𝒜) (p : Y × A) : (controlledPOVM P hP Q).op p = smulKron ((Q p.1).op p.2) (P p.1)

theorem MIPRE.Introspection.sum_blocks_mul_readout {V : Type u_1} {Y : Type u_2} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : Y → Matrix V V ℂ) (hP : IsPVM P) (Q : Y → 𝒜) (y : Y) : (∑ z : Y, smulKron (Q z) (P z)) * smulKron 1 (P y) = smulKron (Q y) (P y)

Multiplication by a readout projector retains exactly its own block.

theorem MIPRE.Introspection.joint_le_second_marginal {Y : Type u_2} {A : Type u_3} [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (Q : POVMIn (Y × A) 𝒜) (y : Y) (a : A) : Q.op (y, a) ≤ (POVMIn.map Prod.snd Q).op a

Every individual joint element is below the marginal that forgets its first outcome.

theorem MIPRE.Introspection.retained_block_le_completion {V : Type u_1} {Y : Type u_2} {A : Type u_3} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (P : Y → Matrix V V ℂ) (hP : IsPVM P) (Q : Y → POVMIn (Y × A) 𝒜) (p : Y × A) : smulKron ((Q p.1).op p) (P p.1) ≤ (controlledPOVM P hP fun (y : Y) => POVMIn.map Prod.snd (Q y)).op p

The matching block is positive and dominated by the controlled marginal POVM.

theorem MIPRE.Introspection.block_retention_precompletion {V : Type u_1} {Y : Type u_2} {A : Type u_3} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {𝒞 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 (Matrix V V 𝒜) ℬ) (M : Y × A → Matrix V V 𝒜) (hM : IsPVMIn M) (P : Y → Matrix V V ℂ) (hP : IsPVM P) (Q : Y → POVMIn (Y × A) 𝒜) (R : Y → ℬ) (hR : IsPVMIn R) (hPR : ∀ (y : Y), (Ψ.π (Ψ.πA (smulKron 1 (P y)))) Ψ.ψ = (Ψ.π (Ψ.πB (R y))) Ψ.ψ) : ∑ p : Y × A, Ψ.stateSqNorm (M p - smulKron ((Q p.1).op p) (P p.1)) ≤ 2 * ∑ y : Y, Ψ.stateSqNorm (∑ a : A, M (y, a) - smulKron 1 (P y)) + 2 * ∑ p : Y × A, Ψ.stateSqNorm (M p - ∑ z : Y, smulKron ((Q z).op p) (P z))

Retain the matching ancillary block, using the exactly consistent mirror readout.

theorem MIPRE.Introspection.block_retention_dist_avg {V : Type u_1} {Y : Type u_2} {A : Type u_3} [Fintype V] [DecidableEq V] [Fintype Y] [DecidableEq Y] [Fintype A] [DecidableEq A] {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {𝒞 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {X : Type u_7} [Fintype X] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (Ψ : BipartiteModel 𝒞 (Matrix V V 𝒜) ℬ) (hΨ : ‖Ψ.ψ‖ = 1) (M : X → Y × A → Matrix V V 𝒜) (hM : ∀ (x : X), IsPVMIn (M x)) (P : X → Y → Matrix V V ℂ) (hP : ∀ (x : X), IsPVM (P x)) (Q : X → Y → POVMIn (Y × A) 𝒜) (R : X → Y → ℬ) (hR : ∀ (x : X), IsPVMIn (R x)) (hPR : ∀ (x : X) (y : Y), (Ψ.π (Ψ.πA (smulKron 1 (P x y)))) Ψ.ψ = (Ψ.π (Ψ.πB (R x y))) Ψ.ψ) {δ : ℝ} (hclose : ∑ x : X, D x * (2 * ∑ y : Y, Ψ.stateSqNorm (∑ a : A, M x (y, a) - smulKron 1 (P x y)) + 2 * ∑ p : Y × A, Ψ.stateSqNorm (M x p - ∑ z : Y, smulKron ((Q x z).op p) (P x z))) ≤ δ) : ∑ x : X, D x * ∑ p : Y × A, Ψ.stateSqNorm (M x p - smulKron ((POVMIn.map Prod.snd (Q x p.1)).op p.2) (P x p.1)) ≤ 2 * δ + 4 * √δ

Complete the retained blocks after averaging questions; the result is an actual family of POVMs.