The value of a POVM strategy, and its conditional failures

MIPRE.TensorProductStrategy is projective by construction, which is the right definition of the quantum value (lem:povm-value-eq says allowing POVMs changes nothing). But a soundness argument often has to start from an arbitrary POVM strategy --- blueprint lem:ms-direct-anticomm is stated for one, and its whole point is that no projectivity is assumed --- so this file gives the unbundled value of a POVM strategy and the conditional failure probabilities that soundness arguments actually consume.

Nothing here is bundled into a structure: the data is a state and two question-indexed families of POVMs on arbitrary finite local spaces, which is how it arrives.

Main definitions

• MIPRE.bornProb: ⟨ψ| E_A ⊗ E_B |ψ⟩, as a real;
• MIPRE.povmValue: the value of a POVM strategy;
• MIPRE.condFail: the failure probability conditioned on a question pair.

Main statements

• MIPRE.sum_bornProb: the Born probabilities of a pair of POVMs sum to one on a unit vector;
• MIPRE.one_sub_povmValue_eq: the failure probability is the average of the conditional ones;
• MIPRE.condFail_le_div: a conditional failure is at most the failure probability divided by the question pair's weight. This is the step that turns "fails with probability ε" into a bound on each subtest, and the division by the weight is why soundness constants carry the number of subtests.

Linearity of the quadratic form and of the Kronecker product

Mathlib states neither over a Finset sum.

theorem MIPRE.sum_quadForm {N : Type u_1} {ι : Type u_2} [Fintype N] (ψ : N → ℂ) (s : Finset ι) (f : ι → Matrix N N ℂ) : star ψ ⬝ᵥ (∑ i ∈ s, f i).mulVec ψ = ∑ i ∈ s, star ψ ⬝ᵥ (f i).mulVec ψ

theorem MIPRE.kronecker_sum_right {dA : Type u_1} {dB : Type u_2} {ι : Type u_3} (M : Matrix dA dA ℂ) (s : Finset ι) (f : ι → Matrix dB dB ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M (∑ i ∈ s, f i) = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M (f i)

theorem MIPRE.sum_kronecker_left {dA : Type u_1} {dB : Type u_2} {ι : Type u_3} (s : Finset ι) (f : ι → Matrix dA dA ℂ) (N : Matrix dB dB ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (∑ i ∈ s, f i) N = ∑ i ∈ s, Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (f i) N

Matrix POVMs are POVMs in the matrix algebra

def MIPRE.POVM.toIn {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) : POVMIn A (Matrix d d ℂ)

A matrix POVM is a POVM in the matrix algebra (MIPRE/Foundations/Measurement.lean): the same three fields.

Equations

• M.toIn = { mats := M.mats, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVM.toIn_op {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) (a : A) : M.toIn.op a = ↑(M.mats a)

theorem MIPRE.POVM.sum_val {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) : ∑ a : A, ↑(M.mats a) = 1

A POVM's elements sum to the identity matrix (its own normalized lives in the self-adjoint subalgebra).

theorem MIPRE.POVM.posSemidef {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) (a : A) : (↑(M.mats a)).PosSemidef

A POVM's elements are positive semidefinite, as bare matrices.

theorem MIPRE.POVM.le_one {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) (p : A) : ↑(M.mats p) ≤ 1

Each POVM element is at most the identity.

theorem MIPRE.POVM.sub_mul_self_le_one {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) (p q : A) : (↑(M.mats p) - ↑(M.mats q)) * (↑(M.mats p) - ↑(M.mats q)) ≤ 1

The difference of two POVM elements is a self-adjoint contraction. This is what makes a two-outcome coarse-graining of a POVM a ±1-observable in every estimate: X† = X and X† X ≤ 1, with no projectivity. Outcomes other than the two chosen contribute nothing.

theorem MIPRE.POVM.sub_conjTranspose {A : Type u_1} {d : Type u_2} [Fintype A] [Fintype d] [DecidableEq d] (M : POVM A d) (p q : A) : (↑(M.mats p) - ↑(M.mats q)).conjTranspose = ↑(M.mats p) - ↑(M.mats q)

The difference of two POVM elements is self-adjoint.

Born probabilities, values and conditional failures in a bipartite model

def MIPRE.BipartiteModel.bornProb {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) (b : ℬ) : ℝ

⟨ψ| πA a πB b |ψ⟩, the Born-rule probability of an outcome pair.

Equations

• M.bornProb a b = M.qform (M.πA a * M.πB b)

theorem MIPRE.BipartiteModel.bornProb_sum_left {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {ι : Type u_4} (s : Finset ι) (f : ι → 𝒜) (b : ℬ) : M.bornProb (∑ i ∈ s, f i) b = ∑ i ∈ s, M.bornProb (f i) b

theorem MIPRE.BipartiteModel.bornProb_sum_right {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {ι : Type u_4} (a : 𝒜) (s : Finset ι) (g : ι → ℬ) : M.bornProb a (∑ i ∈ s, g i) = ∑ i ∈ s, M.bornProb a (g i)

theorem MIPRE.BipartiteModel.bornProb_swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) (b : ℬ) : M.swap.bornProb b a = M.bornProb a b

Exchanging the players exchanges the two factors of a Born probability, because the two players' operators commute.

theorem MIPRE.BipartiteModel.π_πA_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] {a : 𝒜} (ha : 0 ≤ a) : 0 ≤ M.π (M.πA a)

A nonnegative element of the first player's algebra is represented by a positive operator.

theorem MIPRE.BipartiteModel.π_πB_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder ℬ] [StarOrderedRing ℬ] {b : ℬ} (hb : 0 ≤ b) : 0 ≤ M.π (M.πB b)

A nonnegative element of the second player's algebra is represented by a positive operator.

theorem MIPRE.BipartiteModel.bornProb_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {a : 𝒜} {b : ℬ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ M.bornProb a b

Born probabilities of nonnegative elements are nonnegative: the two players' positive operators commute, so their product is positive.

theorem MIPRE.BipartiteModel.sum_bornProb {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {A : Type u_6} {B : Type u_7} [Fintype A] [Fintype B] (hψ : ‖M.ψ‖ = 1) (MA : POVMIn A 𝒜) (MB : POVMIn B ℬ) : ∑ a : A, ∑ b : B, M.bornProb (MA.op a) (MB.op b) = 1

The Born probabilities of a pair of POVMs sum to one on a unit vector.

def MIPRE.BipartiteModel.condWin {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (x : X) (y : Y) : ℝ

The accepted probability at a fixed question pair.

Equations

• M.condWin G MA MB x y = ∑ a : A, ∑ b : B, (if G.D x y a b = true then 1 else 0) * M.bornProb ((MA x).op a) ((MB y).op b)

def MIPRE.BipartiteModel.povmValue {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) : ℝ

The value of a POVM strategy in the model.

Equations

• M.povmValue G MA MB = ∑ x : X, ∑ y : Y, G.μ x y * M.condWin G MA MB x y

def MIPRE.BipartiteModel.condFail {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (MA : X → POVMIn A 𝒜) (MB : Y → POVMIn B ℬ) (x : X) (y : Y) : ℝ

The failure probability conditioned on the question pair (x, y).

Equations

• M.condFail G MA MB x y = 1 - M.condWin G MA MB x y

theorem MIPRE.BipartiteModel.condWin_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (x : X) (y : Y) : 0 ≤ M.condWin G MA MB x y

theorem MIPRE.BipartiteModel.condWin_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) (x : X) (y : Y) : M.condWin G MA MB x y ≤ 1

theorem MIPRE.BipartiteModel.condFail_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) (x : X) (y : Y) : 0 ≤ M.condFail G MA MB x y

theorem MIPRE.BipartiteModel.one_sub_povmValue_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [PartialOrder ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} : 1 - M.povmValue G MA MB = ∑ x : X, ∑ y : Y, G.μ x y * M.condFail G MA MB x y

The failure probability is the average of the conditional failures.

theorem MIPRE.BipartiteModel.condFail_le_div {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {X : Type u_4} {Y : Type u_5} {A : Type u_6} {B : Type u_7} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} {MA : X → POVMIn A 𝒜} {MB : Y → POVMIn B ℬ} (hψ : ‖M.ψ‖ = 1) {ε : ℝ} (hfail : 1 - M.povmValue G MA MB ≤ ε) {x : X} {y : Y} (hμ : 0 < G.μ x y) : M.condFail G MA MB x y ≤ ε / G.μ x y

From a failure bound to a bound on one subtest.

Born probabilities of matrices

The matrix Born probabilities, values and conditional failures are those of the tensor-product model (bornProb_eq_tensor, condWin_eq_tensor, povmValue_eq_tensor, condFail_eq_tensor), and their rules are the model's.

def MIPRE.bornProb {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] (ψ : dA × dB → ℂ) (EA : Matrix dA dA ℂ) (EB : Matrix dB dB ℂ) : ℝ

⟨ψ| E_A ⊗ E_B |ψ⟩, the Born-rule probability of an outcome pair.

Equations

• MIPRE.bornProb ψ EA EB = (star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA EB).mulVec ψ).re

theorem MIPRE.bornProb_eq_tensor {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (EA : Matrix dA dA ℂ) (EB : Matrix dB dB ℂ) : bornProb ψ EA EB = (BipartiteModel.tensor ψ).bornProb EA EB

The matrix Born probability is that of the tensor-product model.

theorem MIPRE.norm_evec_eq_one {N : Type u_7} [Fintype N] {ψ : N → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) : ‖evec ψ‖ = 1

A unit vector of ℂ^N, as a unit vector of EuclideanSpace ℂ N.

theorem MIPRE.bornProb_nonneg {dA : Type u_5} {dB : Type u_6} [Fintype dA] [Fintype dB] (ψ : dA × dB → ℂ) {EA : Matrix dA dA ℂ} {EB : Matrix dB dB ℂ} (hA : EA.PosSemidef) (hB : EB.PosSemidef) : 0 ≤ bornProb ψ EA EB

theorem MIPRE.sum_bornProb {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ψ : dA × dB → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) (MA : POVM A dA) (MB : POVM B dB) : ∑ a : A, ∑ b : B, bornProb ψ ↑(MA.mats a) ↑(MB.mats b) = 1

The Born probabilities of a pair of POVMs sum to one.

The value and the conditional failures

def MIPRE.condWin {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 → ℂ) (MA : X → POVM A dA) (MB : Y → POVM B dB) (x : X) (y : Y) : ℝ

The accepted probability at a fixed question pair.

Equations

• MIPRE.condWin G ψ MA MB x y = ∑ a : A, ∑ b : B, (if G.D x y a b = true then 1 else 0) * MIPRE.bornProb ψ ↑((MA x).mats a) ↑((MB y).mats b)

def MIPRE.povmValue {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 → ℂ) (MA : X → POVM A dA) (MB : Y → POVM B dB) : ℝ

The value of a POVM strategy: the average over question pairs of the accepted probability. For a projective strategy this is TensorProductStrategy.value.

Equations

• MIPRE.povmValue G ψ MA MB = ∑ x : X, ∑ y : Y, G.μ x y * MIPRE.condWin G ψ MA MB x y

def MIPRE.condFail {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 → ℂ) (MA : X → POVM A dA) (MB : Y → POVM B dB) (x : X) (y : Y) : ℝ

The failure probability conditioned on the question pair (x, y).

Equations

• MIPRE.condFail G ψ MA MB x y = 1 - MIPRE.condWin G ψ MA MB x y

theorem MIPRE.condWin_eq_tensor {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 → ℂ} {MA : X → POVM A dA} {MB : Y → POVM B dB} (x : X) (y : Y) : condWin G ψ MA MB x y = (BipartiteModel.tensor ψ).condWin G (fun (x : X) => (MA x).toIn) (fun (y : Y) => (MB y).toIn) x y

theorem MIPRE.povmValue_eq_tensor {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 → ℂ} {MA : X → POVM A dA} {MB : Y → POVM B dB} : povmValue G ψ MA MB = (BipartiteModel.tensor ψ).povmValue G (fun (x : X) => (MA x).toIn) fun (y : Y) => (MB y).toIn

theorem MIPRE.condFail_eq_tensor {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 → ℂ} {MA : X → POVM A dA} {MB : Y → POVM B dB} (x : X) (y : Y) : condFail G ψ MA MB x y = (BipartiteModel.tensor ψ).condFail G (fun (x : X) => (MA x).toIn) (fun (y : Y) => (MB y).toIn) x y

theorem MIPRE.condFail_nonneg {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 → ℂ} {MA : X → POVM A dA} {MB : Y → POVM B dB} (hψ : star ψ ⬝ᵥ ψ = 1) (x : X) (y : Y) : 0 ≤ condFail G ψ MA MB x y

theorem MIPRE.one_sub_povmValue_eq {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 → ℂ} {MA : X → POVM A dA} {MB : Y → POVM B dB} : 1 - povmValue G ψ MA MB = ∑ x : X, ∑ y : Y, G.μ x y * condFail G ψ MA MB x y

The failure probability is the average of the conditional failures.

The value of a commuting-operator strategy is a value in its model

A commuting-operator strategy's measurements are POVMs in the two players' algebras of its model (CommutingOperatorStrategy.toModel), and its value is the model's value of them. So ω_co is the supremum of povmValue over the models of commuting-operator strategies, which is how every statement about povmValue in a model becomes one about ω_co.

noncomputable def MIPRE.CommutingOperatorStrategy.aliceMeas {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) : POVMIn A ↥S.aliceAlg

The first player's measurement at a question, as a POVM in the first player's algebra of the strategy's model.

Equations

• S.aliceMeas x = { mats := fun (a : A) => ⟨⟨S.E x a, ⋯⟩, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

noncomputable def MIPRE.CommutingOperatorStrategy.bobMeas {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) : POVMIn B ↥S.bobAlg

The second player's measurement at a question, as a POVM in the second player's algebra of the strategy's model.

Equations

• S.bobMeas y = { mats := fun (b : B) => ⟨⟨S.F y b, ⋯⟩, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.CommutingOperatorStrategy.aliceMeas_op {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (a : A) : ↑((S.aliceMeas x).op a) = S.E x a

@[simp]

theorem MIPRE.CommutingOperatorStrategy.bobMeas_op {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (y : Y) (b : B) : ↑((S.bobMeas y).op b) = S.F y b

theorem MIPRE.CommutingOperatorStrategy.correlation_eq_bornProb {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (x : X) (y : Y) (a : A) (b : B) : S.correlation x y a b = S.toModel.bornProb ((S.aliceMeas x).op a) ((S.bobMeas y).op b)

The correlation of a strategy is the Born probability of its model.

theorem MIPRE.CommutingOperatorStrategy.value_eq_povmValue {X : Type u_7} {Y : Type u_8} {A : Type u_9} {B : Type u_10} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingOperatorStrategy X Y A B) (G : Game X Y A B) : value G S = S.toModel.povmValue G S.aliceMeas S.bobMeas

The value of a commuting-operator strategy is the value of its measurements in its model.

theorem MIPRE.commutingOperatorValue_eq_iSup_povmValue {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) : commutingOperatorValue G = ⨆ (S : CommutingOperatorStrategy X Y A B), S.toModel.povmValue G S.aliceMeas S.bobMeas

ω_co is the supremum of the model values of commuting-operator strategies.