Value models dominating the POVM strategies of a bipartite model

ValueModel.Dominates ω M (MIPRE/Foundations/ModelStrategy.lean) bounds the projective strategies of M by the value ω. A strategy extracted by a rigidity argument need not be projective: it can be a compression of a projective strategy on an ancilla. So this file bounds the POVM strategies (ValueModel.DominatesPOVM), for the two values:

• val* dominates the POVM strategies of the tensor-product model of a unit vector on any finite registers (ValueModel.tensor_dominatesPOVM): the Naimark dilation of each party's measurements (exists_projective_dilation_povm) makes the strategy projective on the registers extended by the answer sets, at the same value (povmValue_extVec2), and the reindexing of the registers (TensorProductStrategy.ofProjective) makes it a TensorProductStrategy;
• ω_co dominates the POVM strategies of every model on a Hilbert space with a unit state (ValueModel.commuting_dominatesPOVM): such a strategy is a commuting-operator strategy (BipartiteModel.povmValue_le_commutingOperatorValue).

theorem MIPRE.povmValue_le_quantumValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (G : Game X Y A B) (ψ : dA × dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (MA : X → POVM A dA) (MB : Y → POVM B dB) : povmValue G ψ MA MB ≤ quantumValue G

The value of a POVM strategy on a unit vector is at most val*.

def MIPRE.ValueModel.DominatesPOVM {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (ω : ValueModel) (M : BipartiteModel 𝒞 𝒜 ℬ) : Prop

The value model dominates the POVM strategies of a bipartite model: each has value at most the value of its game.

Equations

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

theorem MIPRE.ValueModel.DominatesPOVM.dominates {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {ω : ValueModel} {M : BipartiteModel 𝒞 𝒜 ℬ} (h : ω.DominatesPOVM M) : ω.Dominates M

Dominating the POVM strategies dominates the projective ones.

theorem MIPRE.ValueModel.tensor_dominatesPOVM {dA : Type u_4} {dB : Type u_5} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) : tensor.DominatesPOVM (BipartiteModel.tensor ψ)

val* dominates the POVM strategies of the tensor-product model of a unit vector, on any finite registers.

theorem MIPRE.ValueModel.commuting_dominatesPOVM {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) : commuting.DominatesPOVM M

ω_co dominates the POVM strategies of every bipartite model on a Hilbert space with a unit state.