Exchanging the two players

A game whose question distribution and decision predicate are both symmetric in the players is unchanged by exchanging them, and so is the value of a strategy once the state is swapped (povmValue_swapVec_of_symm). That is what turns a one-sided soundness statement --- one proved about Alice's measurements, with Bob's only as the other party --- into the statement about Bob's, with no second proof: apply it to (MB, MA) on swapVec ψ, and read the conclusion back through norm_stateVecB. In a bipartite model the exchange is BipartiteModel.swap, and the statement is proved once there (BipartiteModel.povmValue_eq_of_bornProb_swap).

The Pauli basis test is such a game: every rule of its decider is written in both orientations (MIPRE.QLD.accepts_symm) and its sampler draws an ordered edge of a symmetric type graph (MIPRE.QLD.qldGame_mu_symm). Its combining stage needs both players' commutation bounds, which is why this is here.

In a bipartite model

In a model the exchange of the players is BipartiteModel.swap, and the two players' operators commute, so a Born probability is symmetric with no reindexing at all (bornProb_swap). The value statement is proved once, for any two models whose Born probabilities agree with the players exchanged (povmValue_eq_of_bornProb_swap): the swapped model is one (povmValue_swap_of_symm), and the tensor-product model of the swapped vector is another, which is the matrix statement below.

theorem MIPRE.BipartiteModel.povmValue_eq_of_bornProb_swap {𝒞 : 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} {A : Type u_5} [Fintype X] [Fintype A] {𝒞' : Type u_6} [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] (M' : BipartiteModel 𝒞' ℬ 𝒜) (hM : ∀ (a : 𝒜) (b : ℬ), M'.bornProb b a = M.bornProb a b) {G : Game X X A A} (MA : X → POVMIn A 𝒜) (MB : X → POVMIn A ℬ) (hμ : ∀ (x y : X), G.μ x y = G.μ y x) (hD : ∀ (x y : X) (a b : A), G.D x y a b = G.D y x b a) : M'.povmValue G MB MA = M.povmValue G MA MB

The value of a strategy for a symmetric game is unchanged by exchanging the players, in any model whose Born probabilities are those of M with the players exchanged. Both halves of the hypothesis on the game are needed: the question distribution is symmetric, and the decider accepts a swapped question pair with the answers swapped too.

theorem MIPRE.BipartiteModel.povmValue_swap_of_symm {𝒞 : 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} {A : Type u_5} [Fintype X] [Fintype A] {G : Game X X A A} (MA : X → POVMIn A 𝒜) (MB : X → POVMIn A ℬ) (hμ : ∀ (x y : X), G.μ x y = G.μ y x) (hD : ∀ (x y : X) (a b : A), G.D x y a b = G.D y x b a) : M.swap.povmValue G MB MA = M.povmValue G MA MB

Exchanging the players in the model: the value of a strategy for a symmetric game is the value of the exchanged strategy in the swapped model.

theorem MIPRE.bornProb_swapVec {dA : Type u_3} {dB : Type u_4} [Fintype dA] [Fintype dB] (ψ : dA × dB → ℂ) (EA : Matrix dA dA ℂ) (EB : Matrix dB dB ℂ) : bornProb (swapVec ψ) EB EA = bornProb ψ EA EB

Swapping the state exchanges the two factors of a Born probability.

@[simp]

theorem MIPRE.swapVec_swapVec {dA : Type u_3} {dB : Type u_4} (ψ : dA × dB → ℂ) : swapVec (swapVec ψ) = ψ

theorem MIPRE.povmValue_swapVec_of_symm {X : Type u_1} {A : Type u_2} {dA : Type u_3} {dB : Type u_4} [Fintype X] [Fintype A] [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {G : Game X X A A} (ψ : dA × dB → ℂ) (MA : X → POVM A dA) (MB : X → POVM A dB) (hμ : ∀ (x y : X), G.μ x y = G.μ y x) (hD : ∀ (x y : X) (a b : A), G.D x y a b = G.D y x b a) : povmValue G (swapVec ψ) MB MA = povmValue G ψ MA MB

The value of a strategy for a symmetric game is unchanged by exchanging the players. Both halves of the hypothesis are needed, and both are properties of the game: the question distribution is symmetric, and the decider accepts a swapped question pair with the answers swapped too.