Replacing one measurement on a common ancillary extension

The new family is a function of the actual question. The selected question uses the supplied projective dilation; every other measurement is the old measurement tensored with identity. The state extension is independent of the question and the opposite player is unchanged.

In a bipartite model (Phase 4 of planning/mipco-track.md) the common extension is the first player's one-sided ancilla Ψ.expandA t₀, and an old measurement tensored with the identity is pushed forward along a ↦ a ⊗ 1 (MIPRE.diagHom).

def MIPRE.Introspection.POVMIn.ampA {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_6} {T : Type u_9} [Fintype A] [Fintype T] [DecidableEq T] (M : POVMIn A 𝒜) : POVMIn A (Matrix T T 𝒜)

An old measurement tensored with the identity of the fresh ancilla.

Equations

• MIPRE.Introspection.POVMIn.ampA M = MIPRE.POVMIn.pushforward MIPRE.diagHom ⋯ M

@[simp]

theorem MIPRE.Introspection.POVMIn.ampA_op {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_6} {T : Type u_9} [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (M : POVMIn A 𝒜) (a : A) : (ampA M).op a = Matrix.diagonal fun (x : T) => M.op a

theorem MIPRE.Introspection.POVMIn.isPVMIn_ampA {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_6} {T : Type u_9} [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] {M : POVMIn A 𝒜} (hM : IsPVMIn M.op) : IsPVMIn (ampA M).op

theorem MIPRE.Introspection.POVMIn.map_ampA {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_6} {C : Type u_8} {T : Type u_9} [Fintype A] [DecidableEq A] [Fintype C] [DecidableEq C] [Fintype T] [DecidableEq T] (M : POVMIn C 𝒜) (f : C → A) : POVMIn.map f (ampA M) = ampA (POVMIn.map f M)

def MIPRE.Introspection.replaceExtended {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {T : Type u_9} [DecidableEq X] [Fintype A] [Fintype T] [DecidableEq T] (MA : X → POVMIn A 𝒜) (q : X) (R : POVMIn A (Matrix T T 𝒜)) : X → POVMIn A (Matrix T T 𝒜)

Actual replacement on one common enlarged register.

Equations

• MIPRE.Introspection.replaceExtended MA q R x = if x = q then R else MIPRE.Introspection.POVMIn.ampA (MA x)

@[simp]

theorem MIPRE.Introspection.replaceExtended_at {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {T : Type u_9} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (MA : X → POVMIn A 𝒜) (q : X) (R : POVMIn A (Matrix T T 𝒜)) : replaceExtended MA q R q = R

theorem MIPRE.Introspection.replaceExtended_other {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {T : Type u_9} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (MA : X → POVMIn A 𝒜) (q x : X) (R : POVMIn A (Matrix T T 𝒜)) (hx : x ≠ q) : replaceExtended MA q R x = POVMIn.ampA (MA x)

theorem MIPRE.Introspection.replaceExtended_isPVM {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_4} {A : Type u_6} {T : Type u_9} [Fintype X] [DecidableEq X] [Fintype A] [DecidableEq A] [Fintype T] [DecidableEq T] (MA : X → POVMIn A 𝒜) (q : X) (R : POVMIn A (Matrix T T 𝒜)) (hMA : ∀ (x : X), IsPVMIn (MA x).op) (hR : IsPVMIn R.op) (x : X) : IsPVMIn (replaceExtended MA q R x).op

theorem MIPRE.Introspection.povmValue_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {T : Type u_9} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype T] [DecidableEq T] (G : Game X Y A B) (t₀ : T) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) : (Ψ.expandA t₀).povmValue G (fun (x : X) => POVMIn.ampA (MA x)) MB = Ψ.povmValue G MA MB

Adding an inert Alice ancilla preserves the whole game's value exactly.

theorem MIPRE.Introspection.replaceExtended_value {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {T : Type u_9} [Fintype X] [DecidableEq X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] [Fintype T] [DecidableEq T] (G : Game X Y A B) (hΨ : ‖Ψ.ψ‖ = 1) (t₀ : T) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (q : X) (M : POVMIn C 𝒜) (R : POVMIn C (Matrix T T 𝒜)) (f : C → A) (hMA : MA q = POVMIn.map f M) (hM : IsPVMIn M.op) (hR : IsPVMIn R.op) (hMB : ∀ (y : Y), IsPVMIn (MB y).op) {δ : ℝ} (hd : ∑ c : C, (Ψ.expandA t₀).stateSqNorm ((Matrix.diagonal fun (x : T) => M.op c) - R.op c) ≤ δ) : |Ψ.povmValue G MA MB - (Ψ.expandA t₀).povmValue G (replaceExtended MA q (POVMIn.map f R)) MB| ≤ 2 * √δ

Quantitative value preservation for the actual replacement family. The fine outcomes may be relabelled by any function, including a constructor in the common parsed-answer alphabet.