Deterministic graph refinement of measurement answers

The old answer is retained verbatim while its deterministic coordinate is recorded in a first component. Thus every old operator occurs exactly once; the construction preserves projectivity and all commutator sums exactly.

Stated for families in any ring, POVMs in an ordered ⋆-ring and a bipartite model (Phase 4 of planning/mipco-track.md).

def MIPRE.Introspection.graphRefinement {A : Type u_1} {C : Type u_2} [DecidableEq C] {R : Type u_4} [Ring R] (M : A → R) (c : A → C) (p : C × A) : R

Record a deterministic coordinate without forgetting the original answer.

Equations

• MIPRE.Introspection.graphRefinement M c p = if p.1 = c p.2 then M p.2 else 0

theorem MIPRE.Introspection.graphRefinement_sum_coordinate {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] (M : A → R) (c : A → C) (a : A) : ∑ z : C, graphRefinement M c (z, a) = M a

theorem MIPRE.Introspection.graphRefinement_sum_fun {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] (M : A → R) (c : A → C) (f : R → ℝ) (hf : f 0 = 0) : ∑ p : C × A, f (graphRefinement M c p) = ∑ a : A, f (M a)

theorem MIPRE.Introspection.graphRefinement_isPVM {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] (M : A → R) (c : A → C) (hM : IsPVMIn M) : IsPVMIn (graphRefinement M c)

theorem MIPRE.Introspection.graphRefinement_eq_fibSum {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] (M : A → R) (c : A → C) (p : C × A) : graphRefinement M c p = fibSumIn M (fun (a : A) => (c a, a)) p

theorem MIPRE.Introspection.graphRefinement_fibSum {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] {B : Type u_5} [DecidableEq B] (M : A → R) (c : A → C) (f : C × A → B) (b : B) : fibSumIn (graphRefinement M c) f b = fibSumIn M (fun (a : A) => f (c a, a)) b

def MIPRE.Introspection.graphRefinementPOVM {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn A R) (c : A → C) : POVMIn (C × A) R

The alphabet change is ordinary deterministic POVM postprocessing.

Equations

• MIPRE.Introspection.graphRefinementPOVM M c = MIPRE.POVMIn.map (fun (a : A) => (c a, a)) M

theorem MIPRE.Introspection.graphRefinementPOVM_mats {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn A R) (c : A → C) (p : C × A) : (graphRefinementPOVM M c).op p = graphRefinement M.op c p

theorem MIPRE.Introspection.graphRefinementPOVM_recover {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn A R) (c : A → C) : POVMIn.map Prod.snd (graphRefinementPOVM M c) = M

theorem MIPRE.Introspection.graphRefinementPOVM_isPVM {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn A R) (c : A → C) (hM : IsPVMIn M.op) : IsPVMIn (graphRefinementPOVM M c).op

theorem MIPRE.Introspection.graphRefinementPOVM_decode {A : Type u_1} {C : Type u_2} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn A R) (c : A → C) (d : C × A → A) (hd : ∀ (a : A), M.op a ≠ 0 → d (c a, a) = a) : POVMIn.map d (graphRefinementPOVM M c) = M

A decoder may change labels only where the old effect vanishes.

theorem MIPRE.Introspection.graphRefinement_commutator_sum {A : Type u_1} {C : Type u_2} {B : Type u_3} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] {𝒞 : Type u_4} {𝒜 : Type u_5} {ℬ : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Fintype B] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) (M : A → 𝒜) (c : A → C) (N : B → 𝒜) : ∑ p : C × A, ∑ b : B, Ψ.stateSqNorm (graphRefinement M c p * N b - N b * graphRefinement M c p) = ∑ a : A, ∑ b : B, Ψ.stateSqNorm (M a * N b - N b * M a)

Refinement introduces no commutator loss, for any comparison operators.