Mixtures and extensions of POVMs, and the agreement triangle #
Three constructions on bundled POVMs that the padded strategy of the Pauli basis test's stage 4 needs, and one inequality.
POVM.aOpextends a POVM ondby the identity tod × E;POVM.dirac a₀answersa₀with certainty;POVM.mix w Qis a convex combination of POVMs with the same outcomes. A strategy that must be a function of the question while the analysis controls it sample by sample is a mixture over the samples producing the question, and the Born rule's linearity (bornProb_mix_left,bornProb_mix_right) turns a bound on the mixture into the average of the per-sample bounds.agreeSum_triangleis the paper's triangle-like inequality for the consistency relation (fact:triangle-for-simeq, item 1): if Alice'sAagrees with Bob'sB, Alice'sCagrees with Bob'sB, and Alice'sCagrees with Bob'sD, each with probability at least1 - δ, then Alice'sAagrees with Bob'sDwith probability at least1 - 11 δ. No projectivity is assumed: for POVMs the agreement is not a squared distance, and the argument goes through the vectors(R_a ⊗ I)|ψ⟩, whose weighted squared norms are at most one and, by Cauchy--Schwarz against a partner they agree with, at least1 - 2δ. The paper pads these vectors to unit vectors and gets9 δ; the unpadded argument here costs the extra2 δand needs no auxiliary space.
The Born-rule facts, the failure bounds and the agreement triangle are proved once, for a
bipartite model (BipartiteModel.bornProb_mix_left, BipartiteModel.agreeSum_triangle, ...), with
POVMIn.dirac and POVMIn.mix the constructions in a player's algebra; the matrix statements are
their instances in the tensor-product model.
Mixtures in a ⋆-algebra #
def
MIPRE.POVMIn.dirac
{R : Type u_1}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
{A : Type u_2}
[Fintype A]
[DecidableEq A]
(a₀ : A)
:
POVMIn A R
The deterministic POVM answering a₀.
Equations
Instances For
theorem
MIPRE.POVMIn.dirac_op
{R : Type u_1}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
{A : Type u_2}
[Fintype A]
[DecidableEq A]
(a₀ a : A)
:
theorem
MIPRE.POVMIn.real_smul_nonneg
{R : Type u_1}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
[Algebra ℂ R]
[StarModule ℂ R]
{r : ℝ}
(hr : 0 ≤ r)
{x : R}
(hx : 0 ≤ x)
:
A real multiple of a nonnegative element, with a nonnegative real, is nonnegative:
r • x = √r x √r.
def
MIPRE.POVMIn.mix
{R : Type u_1}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
[Algebra ℂ R]
[StarModule ℂ R]
{A : Type u_2}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVMIn A R)
:
POVMIn A R
A convex combination of POVMs with the same outcomes, with real weights w summing to
one.
Equations
Instances For
theorem
MIPRE.POVMIn.mix_op
{R : Type u_1}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
[Algebra ℂ R]
[StarModule ℂ R]
{A : Type u_2}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVMIn A R)
(a : A)
:
Mixtures and relabellings in a bipartite model #
theorem
MIPRE.BipartiteModel.bornProb_smul_left
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
(r : ℝ)
(a : 𝒜)
(b : ℬ)
:
The Born probability is linear in a real multiple of the first player's operator.
theorem
MIPRE.BipartiteModel.bornProb_smul_right
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
(r : ℝ)
(a : 𝒜)
(b : ℬ)
:
The Born probability is linear in a real multiple of the second player's operator.
theorem
MIPRE.BipartiteModel.bornProb_mix_left
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarModule ℂ 𝒜]
{A : Type u_4}
[Fintype A]
{ι : Type u_5}
[Fintype ι]
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVMIn A 𝒜)
(a : A)
(b : ℬ)
:
The Born probability of a mixture is the mixture of the Born probabilities, on the first player's side.
theorem
MIPRE.BipartiteModel.bornProb_mix_right
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarModule ℂ ℬ]
{A : Type u_4}
[Fintype A]
{ι : Type u_5}
[Fintype ι]
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(a : 𝒜)
(Q : ι → POVMIn A ℬ)
(b : A)
:
The same, on the second player's side.
theorem
MIPRE.BipartiteModel.condFail_le_one_sub_sum_bornProb_map
{𝒞 : 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}
{C : Type u_8}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype C]
[DecidableEq C]
{G : Game X Y A B}
{MA : X → POVMIn A 𝒜}
{MB : Y → POVMIn B ℬ}
{x : X}
{y : Y}
(f : A → C)
(g : B → C)
(hD : ∀ (a : A) (b : B), (MA x).op a ≠ 0 → (MB y).op b ≠ 0 → f a = g b → G.D x y a b = true)
:
M.condFail G MA MB x y ≤ 1 - ∑ c : C, M.bornProb ((POVMIn.map f (MA x)).op c) ((POVMIn.map g (MB y)).op c)
Agreement on the support implies acceptance bounds the conditional failure by the disagreement of the relabelled POVMs. Only outcomes both parties can produce are asked to be accepted.
theorem
MIPRE.BipartiteModel.condFail_le_one_sub_sum_bornProb_diag
{𝒞 : 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}
[Fintype X]
[Fintype Y]
[Fintype A]
{MA : X → POVMIn A 𝒜}
{x : X}
{y : Y}
{G : Game X Y A A}
{MB : Y → POVMIn A ℬ}
(hD : ∀ (a : A), (MA x).op a ≠ 0 → (MB y).op a ≠ 0 → G.D x y a a = true)
:
The same with both parties' outcomes read as they are: acceptance of every diagonal pair on the support bounds the conditional failure by the diagonal disagreement.
The agreement triangle #
def
MIPRE.BipartiteModel.agreeSum
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
(μ : X → ℝ)
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
The agreement probability of two families of POVMs, one per party, on the same questions,
averaged over the question distribution μ: the paper's p(R, S).
Instances For
def
MIPRE.BipartiteModel.weightA
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
[PartialOrder 𝒜]
{X : Type u_4}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
(μ : X → ℝ)
(MA : X → POVMIn Λ 𝒜)
:
The weighted squared norm of the first player's measurement vectors.
Equations
- M.weightA μ MA = ∑ x : X, μ x * ∑ a : Λ, M.stateSqNorm ((MA x).op a)
Instances For
def
MIPRE.BipartiteModel.xDev
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
(μ : X → ℝ)
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
The weighted cross-party deviation of two families.
Instances For
theorem
MIPRE.BipartiteModel.agreeSum_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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
Exchanging the players leaves the agreement unchanged.
theorem
MIPRE.BipartiteModel.weightA_nonneg
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
[PartialOrder 𝒜]
{X : Type u_4}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(MA : X → POVMIn Λ 𝒜)
:
theorem
MIPRE.BipartiteModel.xDev_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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
The cross deviation expands: xDev = weightA + weightB - 2 agreeSum, with the second
player's weight the first player's in the swapped model.
theorem
MIPRE.BipartiteModel.bornProb_le_stateNorm_mul
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
{a : 𝒜}
(ha : star a = a)
(b : ℬ)
:
A Born probability is at most the product of the two state norms (Cauchy--Schwarz).
theorem
MIPRE.BipartiteModel.agreeSum_le_sqrt_mul_sqrt
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
Cauchy--Schwarz for the agreement: agreeSum ≤ √weightA · √weightB.
theorem
MIPRE.BipartiteModel.weightA_le_one
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
(M : BipartiteModel 𝒞 𝒜 ℬ)
[PartialOrder 𝒜]
{X : Type u_4}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
[StarOrderedRing 𝒜]
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : ‖M.ψ‖ = 1)
(MA : X → POVMIn Λ 𝒜)
:
theorem
MIPRE.BipartiteModel.weightA_ge
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
[StarOrderedRing ℬ]
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : ‖M.ψ‖ = 1)
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
{δ : ℝ}
(h : 1 - M.agreeSum μ MA MB ≤ δ)
:
A family that agrees with some partner with probability at least 1 - δ has weight at least
1 - 2δ.
theorem
MIPRE.BipartiteModel.xDev_le
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
[StarOrderedRing 𝒜]
[StarOrderedRing ℬ]
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : ‖M.ψ‖ = 1)
(MA : X → POVMIn Λ 𝒜)
(MB : X → POVMIn Λ ℬ)
:
The cross deviation is at most twice the disagreement.
theorem
MIPRE.BipartiteModel.xDev_triangle
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(A C : X → POVMIn Λ 𝒜)
(B D : X → POVMIn Λ ℬ)
:
The weighted triangle inequality for cross deviations: the first player's A against the
second player's D, through the second player's B and the first player's C.
theorem
MIPRE.BipartiteModel.agreeSum_triangle
{𝒞 : 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}
{Λ : Type u_5}
[Fintype X]
[Fintype Λ]
{μ : X → ℝ}
[StarOrderedRing 𝒜]
[StarOrderedRing ℬ]
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : ‖M.ψ‖ = 1)
(A C : X → POVMIn Λ 𝒜)
(B D : X → POVMIn Λ ℬ)
{δ : ℝ}
(hAB : 1 - M.agreeSum μ A B ≤ δ)
(hCB : 1 - M.agreeSum μ C B ≤ δ)
(hCD : 1 - M.agreeSum μ C D ≤ δ)
:
The agreement triangle (fact:triangle-for-simeq, item 1, with 11 δ in place of the
paper's 9 δ): agreement is transitive across the two parties, for POVMs.
Extension by the identity, and the deterministic POVM #
def
MIPRE.POVM.aOp
{A : Type u_1}
[Fintype A]
{d : Type u_2}
{E : Type u_3}
[Fintype d]
[DecidableEq d]
[Fintype E]
[DecidableEq E]
(M : POVM A d)
:
A POVM on d, extended by the identity to d × E.
Equations
Instances For
theorem
MIPRE.POVM.map_aOp
{A : Type u_1}
[Fintype A]
{d : Type u_2}
{E : Type u_3}
[Fintype d]
[DecidableEq d]
[Fintype E]
[DecidableEq E]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
(f : A → B)
(M : POVM A d)
:
Extending by the identity commutes with relabelling the outcomes.
def
MIPRE.POVM.dirac
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
[DecidableEq A]
(a₀ : A)
:
POVM A d
The deterministic POVM answering a₀.
Equations
Instances For
Mixtures #
noncomputable def
MIPRE.POVM.mix
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{ι : Type u_3}
[Fintype ι]
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVM A d)
:
POVM A d
A convex combination of POVMs with the same outcomes, with real weights w summing to
one.
Equations
Instances For
theorem
MIPRE.bornProb_mix_left
{A : Type u_1}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
{dA : Type u_4}
{dB : Type u_5}
[Fintype dA]
[Fintype dB]
[DecidableEq dA]
[DecidableEq dB]
(ψ : dA × dB → ℂ)
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVM A dA)
(a : A)
(EB : Matrix dB dB ℂ)
:
The Born probability of a mixture is the mixture of the Born probabilities, on Alice's side.
theorem
MIPRE.bornProb_mix_right
{A : Type u_1}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
{dA : Type u_4}
{dB : Type u_5}
[Fintype dA]
[Fintype dB]
[DecidableEq dA]
[DecidableEq dB]
(ψ : dA × dB → ℂ)
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(EA : Matrix dA dA ℂ)
(Q : ι → POVM A dB)
(a : A)
:
The same, on Bob's side.
A POVM from a positive family, and uniform averages #
def
MIPRE.POVM.ofPosSemidef
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
(E : A → Matrix d d ℂ)
(hpos : ∀ (a : A), (E a).PosSemidef)
(hsum : ∑ a : A, E a = 1)
:
POVM A d
A POVM from a family of positive semidefinite matrices summing to the identity.
Equations
Instances For
@[simp]
theorem
MIPRE.POVM.ofPosSemidef_mats
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
(E : A → Matrix d d ℂ)
(hpos : ∀ (a : A), (E a).PosSemidef)
(hsum : ∑ a : A, E a = 1)
(a : A)
:
The uniform weights on a finset.
Instances For
theorem
MIPRE.sum_unifOn
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
(S : Finset ι)
(hS : S.Nonempty)
:
noncomputable def
MIPRE.POVM.avgOn
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[DecidableEq A]
(S : Finset ι)
(Q : ι → POVM A d)
(a₀ : A)
:
POVM A d
The uniform average of POVMs over a finset, defaulting to the deterministic answer a₀
when the finset is empty.
Equations
- MIPRE.POVM.avgOn S Q a₀ = if hS : S.Nonempty then MIPRE.POVM.mix (MIPRE.unifOn S) ⋯ ⋯ Q else MIPRE.POVM.dirac a₀
Instances For
theorem
MIPRE.bornProb_avgOn_left
{A : Type u_1}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[DecidableEq A]
{dA : Type u_4}
{dB : Type u_5}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(ψ : dA × dB → ℂ)
{S : Finset ι}
(hS : S.Nonempty)
(Q : ι → POVM A dA)
(a₀ a : A)
(EB : Matrix dB dB ℂ)
:
theorem
MIPRE.bornProb_avgOn_right
{A : Type u_1}
[Fintype A]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[DecidableEq A]
{dA : Type u_4}
{dB : Type u_5}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(ψ : dA × dB → ℂ)
(EA : Matrix dA dA ℂ)
{S : Finset ι}
(hS : S.Nonempty)
(Q : ι → POVM A dB)
(a₀ a : A)
:
Averages and relabelling #
theorem
MIPRE.POVM.avgOn_mats
{A : Type u_1}
[Fintype A]
[DecidableEq A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
{S : Finset ι}
(hS : S.Nonempty)
(Q : ι → POVM A d)
(a₀ a : A)
:
The operators of a uniform average over a nonempty finset.
theorem
MIPRE.POVM.map_mix
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{ι : Type u_3}
[Fintype ι]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
(g : A → B)
(w : ι → ℝ)
(hw : ∀ (i : ι), 0 ≤ w i)
(hw1 : ∑ i : ι, w i = 1)
(Q : ι → POVM A d)
:
Relabelling commutes with mixing.
theorem
MIPRE.POVM.map_dirac
{A : Type u_1}
[Fintype A]
[DecidableEq A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
(g : A → B)
(a₀ : A)
:
Relabelling the deterministic POVM.
theorem
MIPRE.POVM.map_avgOn
{A : Type u_1}
[Fintype A]
[DecidableEq A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
(g : A → B)
(S : Finset ι)
(Q : ι → POVM A d)
(a₀ : A)
:
Relabelling commutes with the uniform average.
theorem
MIPRE.POVM.map_id
{A : Type u_1}
[Fintype A]
[DecidableEq A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
(M : POVM A d)
:
Relabelling along the identity does nothing.
theorem
MIPRE.POVM.map_mats_eq_zero_of_forall_ne
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
(f : A → B)
(M : POVM A d)
{b : B}
(h : ∀ (a : A), f a ≠ b)
:
An outcome outside the range of the relabelling carries the zero operator.
theorem
MIPRE.POVM.map_congr_of_support
{A : Type u_1}
[Fintype A]
{d : Type u_2}
[Fintype d]
[DecidableEq d]
{B : Type u_4}
[Fintype B]
[DecidableEq B]
{f g : A → B}
(M : POVM A d)
(h : ∀ (a : A), ↑(M.mats a) ≠ 0 → f a = g a)
:
Two relabellings that agree on the support of a POVM relabel it the same way.
Acceptance on the support, and the conditional failure #
theorem
MIPRE.condFail_le_one_sub_sum_bornProb_map
{dA : Type u_1}
{dB : Type u_2}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{X : Type u_3}
{Y : Type u_4}
{A : Type u_5}
{B : Type u_6}
{C : Type u_7}
[Fintype X]
[Fintype Y]
[Fintype A]
[Fintype B]
[Fintype C]
[DecidableEq C]
{ψ : dA × dB → ℂ}
{x : X}
{y : Y}
{G : Game X Y A B}
{MA : X → POVM A dA}
{MB : Y → POVM B dB}
(f : A → C)
(g : B → C)
(hD : ∀ (a : A) (b : B), ↑((MA x).mats a) ≠ 0 → ↑((MB y).mats b) ≠ 0 → f a = g b → G.D x y a b = true)
:
Agreement on the support implies acceptance bounds the conditional failure by the disagreement of the relabelled POVMs. Only outcomes both parties can produce are asked to be accepted, which is what a strategy answering every question in its own format needs.
theorem
MIPRE.condFail_le_one_sub_sum_bornProb_diag
{dA : Type u_1}
{dB : Type u_2}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{X : Type u_3}
{Y : Type u_4}
{A : Type u_5}
[Fintype X]
[Fintype Y]
[Fintype A]
{ψ : dA × dB → ℂ}
{x : X}
{y : Y}
{G : Game X Y A A}
{MA : X → POVM A dA}
{MB : Y → POVM A dB}
(hD : ∀ (a : A), ↑((MA x).mats a) ≠ 0 → ↑((MB y).mats a) ≠ 0 → G.D x y a a = true)
:
The same with both parties' outcomes read as they are: acceptance of every diagonal pair on the support bounds the conditional failure by the diagonal disagreement.
theorem
MIPRE.sum_bornProb_map'
{dA : Type u_1}
{dB : Type u_2}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{C : Type u_7}
[Fintype C]
[DecidableEq C]
{ψ : dA × dB → ℂ}
{A : Type u_8}
{B : Type u_9}
[Fintype A]
[Fintype B]
(P : POVM A dA)
(Q : POVM B dB)
(f : A → C)
(g : B → C)
:
sum_bornProb_map for two bare POVMs.
theorem
MIPRE.bornProb_one_one
{dA : Type u_1}
{dB : Type u_2}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{ψ : dA × dB → ℂ}
(hψ : star ψ ⬝ᵥ ψ = 1)
:
The agreement triangle #
def
MIPRE.agreeSum
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(μ : X → ℝ)
(ψ : dA × dB → ℂ)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
:
The agreement probability of two families of POVMs, one per party, on the same questions,
averaged over the question distribution μ: the paper's p(R, S).
Equations
- MIPRE.agreeSum μ ψ M N = ∑ x : X, μ x * ∑ a : Λ, MIPRE.bornProb ψ ↑((M x).mats a) ↑((N x).mats a)
Instances For
noncomputable def
MIPRE.weightA
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(μ : X → ℝ)
(ψ : dA × dB → ℂ)
(M : X → POVM Λ dA)
:
The weighted squared norm of Alice's measurement vectors, ∑_x μ_x ∑_a ‖(M^x_a ⊗ I)ψ‖².
Equations
- MIPRE.weightA μ ψ M = ∑ x : X, μ x * ∑ a : Λ, MIPRE.stateSqNorm ψ ↑((M x).mats a)
Instances For
noncomputable def
MIPRE.weightB
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(μ : X → ℝ)
(ψ : dA × dB → ℂ)
(N : X → POVM Λ dB)
:
Bob's version.
Equations
- MIPRE.weightB μ ψ N = ∑ x : X, μ x * ∑ a : Λ, ‖MIPRE.stateVecB ψ ↑((N x).mats a)‖ ^ 2
Instances For
noncomputable def
MIPRE.xDev
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(μ : X → ℝ)
(ψ : dA × dB → ℂ)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
:
The weighted cross-party deviation of two families.
Equations
- MIPRE.xDev μ ψ M N = ∑ x : X, μ x * ∑ a : Λ, MIPRE.xSqNorm ψ ↑((M x).mats a) ↑((N x).mats a)
Instances For
theorem
MIPRE.weightA_eq_tensor
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(M : X → POVM Λ dA)
:
theorem
MIPRE.weightB_eq_tensor
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(N : X → POVM Λ dB)
:
theorem
MIPRE.weightA_le_one
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(M : X → POVM Λ dA)
:
theorem
MIPRE.weightB_le_one
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(N : X → POVM Λ dB)
:
theorem
MIPRE.xDev_eq
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
:
The cross deviation expands: xDev = weightA + weightB - 2 agreeSum.
theorem
MIPRE.bornProb_le_norm_mul_norm
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
(ψ : dA × dB → ℂ)
{EA : Matrix dA dA ℂ}
(hEA : EA.conjTranspose = EA)
(EB : Matrix dB dB ℂ)
:
A Born probability is at most the product of the two state norms (Cauchy--Schwarz).
theorem
MIPRE.agreeSum_le_sqrt_mul_sqrt
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
:
Cauchy--Schwarz for the agreement: agreeSum ≤ √weightA · √weightB.
theorem
MIPRE.weightA_ge
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
{δ : ℝ}
(h : 1 - agreeSum μ ψ M N ≤ δ)
:
A family that agrees with some partner with probability at least 1 - δ has weight at least
1 - 2δ.
theorem
MIPRE.weightB_ge
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
{δ : ℝ}
(h : 1 - agreeSum μ ψ M N ≤ δ)
:
Bob's version.
theorem
MIPRE.xDev_le
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(M : X → POVM Λ dA)
(N : X → POVM Λ dB)
:
The cross deviation is at most twice the disagreement.
theorem
MIPRE.xDev_triangle
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(A C : X → POVM Λ dA)
(B D : X → POVM Λ dB)
:
The weighted triangle inequality for cross deviations: Alice's A against Bob's D,
through Bob's B and Alice's C.
theorem
MIPRE.agreeSum_triangle
{X : Type u_1}
{Λ : Type u_2}
[Fintype X]
[Fintype Λ]
{dA : Type u_3}
{dB : Type u_4}
[Fintype dA]
[DecidableEq dA]
[Fintype dB]
[DecidableEq dB]
{μ : X → ℝ}
{ψ : dA × dB → ℂ}
(hμ : ∀ (x : X), 0 ≤ μ x)
(hμ1 : ∑ x : X, μ x = 1)
(hψ : star ψ ⬝ᵥ ψ = 1)
(A C : X → POVM Λ dA)
(B D : X → POVM Λ dB)
{δ : ℝ}
(hAB : 1 - agreeSum μ ψ A B ≤ δ)
(hCB : 1 - agreeSum μ ψ C B ≤ δ)
(hCD : 1 - agreeSum μ ψ C D ≤ δ)
:
The agreement triangle (fact:triangle-for-simeq, item 1, with 11 δ in place of the
paper's 9 δ): agreement is transitive across the two parties, for POVMs.