Reducing the POVM strategies of one bipartite model to another's

Introspection extracts its strategy in a model built from the ancilla of the Pauli basis test by adjoining, stage by stage, an ancilla register to one player (BipartiteModel.expandA, and its second-player form on the swapped model), and the value model has to dominate the model the strategy ends up in. Every POVM strategy of an extended model has the value of a POVM strategy of the original one — its compression to the ancilla's reference state (POVMIn.compress), which is a POVM because the diagonal blocks of a nonnegative block matrix are nonnegative (MatrixStar.diag_nonneg) — so domination passes to the extension for every value model (ValueModel.DominatesPOVM.of_povmReduces), with no hypothesis on the value model. A local isometry carrying the state to the state reduces its source to its target the same way, by the pushforward (BipartiteModel.LocalIsometry.povmReduces).

Phase 4 of planning/mipco-track.md.

Compressing a POVM of block matrices

def MIPRE.POVMIn.compress {A : Type u_1} {T : Type u_2} {R : Type u_3} [Fintype A] [Fintype T] [DecidableEq T] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] (t₀ : T) (P : POVMIn A (Matrix T T R)) : POVMIn A R

The compression of a POVM of block matrices to one diagonal block: a POVM, since the diagonal blocks of a nonnegative block matrix are nonnegative and those of 1 are 1.

Equations

• MIPRE.POVMIn.compress t₀ P = { mats := fun (a : A) => ⟨P.op a t₀ t₀, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVMIn.compress_op {A : Type u_1} {T : Type u_2} {R : Type u_3} [Fintype A] [Fintype T] [DecidableEq T] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [StarProper R] (t₀ : T) (P : POVMIn A (Matrix T T R)) (a : A) : (compress t₀ P).op a = P.op a t₀ t₀

The reduction

def MIPRE.BipartiteModel.POVMReduces {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [PartialOrder ℬ'] (M' : BipartiteModel 𝒞' 𝒜' ℬ') (M : BipartiteModel 𝒞 𝒜 ℬ) : Prop

The POVM strategies of M' reduce to those of M: each, for any game on Type, has value at most that of a POVM strategy of M.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.BipartiteModel.POVMReduces.refl {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.POVMReduces M

theorem MIPRE.BipartiteModel.POVMReduces.trans {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] [PartialOrder 𝒜''] [StarOrderedRing 𝒜''] [PartialOrder ℬ''] [StarOrderedRing ℬ''] {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M : BipartiteModel 𝒞 𝒜 ℬ} (h₁ : M''.POVMReduces M') (h₂ : M'.POVMReduces M) : M''.POVMReduces M

theorem MIPRE.BipartiteModel.LocalIsometry.povmReduces {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (h : Φ.W M.ψ = M'.ψ) (hA : Φ.ΦA 1 = 1) (hB : Φ.ΦB 1 = 1) : M.POVMReduces M'

A local isometry carrying the state to the state reduces its source to its target: a strategy moves by the pushforward, with its value (LocalIsometry.povmValue_pushforward).

theorem MIPRE.BipartiteModel.povmReduces_expandA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {T : Type u_7} [Fintype T] [DecidableEq T] [StarProper 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : (M.expandA t₀).POVMReduces M

Adjoining an ancilla register to the first player reduces to the original model: a strategy's value is that of its compression to the reference state (bornProb_expandA).

theorem MIPRE.BipartiteModel.povmReduces_expandB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {T : Type u_7} [Fintype T] [DecidableEq T] [StarProper ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (t₀ : T) : (M.swap.expandA t₀).swap.POVMReduces M

Adjoining an ancilla register to the second player reduces to the original model: the extension of the first player of the swapped model, swapped back.

Exchanging the players

def MIPRE.Game.swap {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : Game Y X B A

The game with the players exchanged: the second player is asked the first question and answers first.

Equations

• G.swap = { μ := fun (y : Y) (x : X) => G.μ x y, μ_nonneg := ⋯, μ_sum_one := ⋯, D := fun (y : Y) (x : X) (b : B) (a : A) => G.D x y a b }

theorem MIPRE.BipartiteModel.povmValue_swap_game {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (PA : X → POVMIn A 𝒜) (PB : Y → POVMIn B ℬ) : M.swap.povmValue G.swap PB PA = M.povmValue G PA PB

A strategy's value in the swapped model is that of the exchanged strategy for the exchanged game.

theorem MIPRE.BipartiteModel.POVMReduces.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M : BipartiteModel 𝒞 𝒜 ℬ} (h : M'.POVMReduces M) : M'.swap.POVMReduces M.swap

A reduction survives exchanging the players.

theorem MIPRE.ValueModel.DominatesPOVM.of_povmReduces {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {ω : ValueModel} {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (h : M'.POVMReduces M) (hM : ω.DominatesPOVM M) : ω.DominatesPOVM M'

Domination passes along a reduction: a value model dominating the POVM strategies of M dominates those of every model reducing to M.