Pasting two measurements into one

The blueprint's missing piece for lem:qld-pairs-of-lines: NW19's Fact 4.35, the paper's lem:pasting-updated. One party holds a joint projective measurement A_{a,b}; the other holds two projective measurements G_1 and G_2 whose coarse-grainings along evaluation maps agree with A's two marginals. The conclusion is that A agrees with the sandwich J_{g_1, g_2} = G_2^{g_2} G_1^{g_1} G_2^{g_2}, coarse-grained by evaluating both outcomes.

Two facts beyond the sandwich chain of MIPRE/Foundations/Sandwich.lean are needed, and they are proved first.

• A sub-measurement close to a projective measurement carries almost all the mass (qform_sum_ge_of_close, NW19's Fact 4.31). Two Cauchy--Schwarz steps against the same deviation, and the loss is 2 sqrt(delta).
• Multiplying by the projector of the same outcome costs nothing (sum_snorm_sq_cool, the paper's lem:cool-closeness-fact in its partition form). The cross terms vanish by mutual orthogonality and each diagonal term loses only A_a <= Id. The partition form is what matters: the consumers apply it to the q fibres of an outcome map at once, and the single-subset form would cost a factor q there.

The sandwich is where a collision probability enters. G_2^{g_2} G_1 G_2^{g_2} summed over a fibre of g_2 |-> g_2(y) is a pinching of G_1 by that fibre, not a conjugation by the fibre's projector, and the difference is the cross terms g_2 \ne g_2' with g_2(y) = g_2'(y). Those are rare exactly when the outcome map separates the family, which for line polynomials is Schwartz--Zippel.

The argument is proved once, for a bipartite model (MIPRE/Foundations/BipartiteModel.lean) with the first player's joint measurement in 𝒜 and the second player's two families in ℬ: the pasting lemma is BipartiteModel.one_sub_sum_bornProb_pasteJ_le, and NW19's Fact 4.31 is StateModel.qform_sum_ge_of_close. The coarse-graining fibSumIn (of which the matrix fibSum is the instance) and the pasted family pasteJ are defined in any ring, and the sandwich identities they rest on are those of projective measurements in a ⋆-ring (IsPVMIn.conj_eq_gram, IsPVMIn.sum_pasteJ). The matrix statements are the instances in the tensor-product model BipartiteModel.tensor ψ. Where the square of a positive contraction is bounded (P² ≤ P for 0 ≤ P ≤ 1), the hypothesis is on the operators represented on the Hilbert space, where the functional calculus proves it, and the matrix instances discharge it from matrix positivity; the matrix inequality sum_sq_le_one_of_sum_eq_one is itself the instance of sum_mul_self_le_one_of_sum_le_one, stated in any ordered algebra with a functional calculus. Only the transport to a twice-extended state (xSqNorm_extVec2_aOp) is about matrices alone.

The coarse-graining of a family, and the product question distribution

def MIPRE.fibSumIn {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [DecidableEq β] [AddCommMonoid M] (G : α → M) (e : α → β) (b : β) : M

The fibre sum of a family along an outcome map --- its coarse-graining --- in any additive monoid, so that the family may be matrices or elements of a player's algebra.

Equations

• MIPRE.fibSumIn G e b = ∑ g : α with e g = b, G g

theorem MIPRE.isPVMIn_fibSumIn {S : Type u_1} {α : Type u_2} {β : Type u_3} [Ring S] [StarRing S] [Fintype α] [Fintype β] [DecidableEq β] {G : α → S} (h : IsPVMIn G) (e : α → β) : IsPVMIn (fibSumIn G e)

The coarse-graining of a projective measurement in a ⋆-ring is projective.

def MIPRE.fibSum {α : Type u_1} {β : Type u_2} {N : Type u_3} [Fintype α] [DecidableEq β] (G : α → Matrix N N ℂ) (e : α → β) (b : β) : Matrix N N ℂ

The fibre sum of a family of operators along an outcome map --- its coarse-graining. It is fibSumIn in a matrix algebra (fibSum_eq_fibSumIn); the square matrix type stays in the signature, because consumers let it fix the dimension.

Equations

• MIPRE.fibSum G e b = ∑ g : α with e g = b, G g

theorem MIPRE.fibSum_eq_fibSumIn {α : Type u_1} {β : Type u_2} {N : Type u_3} [Fintype α] [DecidableEq β] (G : α → Matrix N N ℂ) (e : α → β) (b : β) : fibSum G e b = fibSumIn G e b

theorem MIPRE.isPVM_fibSum {N : Type u_1} [Fintype N] [DecidableEq N] {α : Type u_2} {β : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {G : α → Matrix N N ℂ} (h : IsPVM G) (e : α → β) : IsPVM (fibSum G e)

theorem MIPRE.sum_prod_uniform {Z : Type u_4} {Y : Type u_5} [Fintype Z] [Fintype Y] [Nonempty Y] (ν f : Z → ℝ) : ∑ i : Z × Y, ν i.1 * (↑(Fintype.card Y))⁻¹ * f i.1 = ∑ z : Z, ν z * f z

The question distribution of the pasting lemma: a weight on the part both measurements see, times the uniform distribution on the probe that separates the second family's outcomes.

theorem MIPRE.sum_prod_uniform_one {Z : Type u_4} {Y : Type u_5} [Fintype Z] [Fintype Y] [Nonempty Y] {ν : Z → ℝ} (hν : ∑ z : Z, ν z = 1) : ∑ i : Z × Y, ν i.1 * (↑(Fintype.card Y))⁻¹ = 1

The product question distribution is a distribution.

Regrouping along the fibres of an outcome map

theorem MIPRE.sum_prod_eq {M : Type u_1} [AddCommMonoid M] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (f : α → β → M) : ∑ a : α, ∑ b : β, f a b = ∑ p : α × β, f p.1 p.2

theorem MIPRE.sum_fiber {α : Type u_1} {β : Type u_2} {M : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] [AddCommMonoid M] (e : α → β) (f : β → α → M) : ∑ g : α, f (e g) g = ∑ b : β, ∑ g : α with e g = b, f b g

A sum whose summand depends on the index only through its image splits into the fibres.

theorem MIPRE.sum_comm4 {α : Type u_1} {β : Type u_2} {γ : Type u_3} {κ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] [Fintype κ] (T : α → β → γ → κ → ℝ) : ∑ y : α, ∑ a : β, ∑ g : γ, ∑ g' : κ, T y a g g' = ∑ a : β, ∑ g : γ, ∑ g' : κ, ∑ y : α, T y a g g'

Moving the outermost sum of four inwards.

theorem MIPRE.abs_sum_sum_le_sqrt {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (f u v : α → β → ℝ) (hf : ∀ (a : α) (b : β), |f a b| ≤ u a b * v a b) : |∑ a : α, ∑ b : β, f a b| ≤ √(∑ a : α, ∑ b : β, u a b ^ 2) * √(∑ a : α, ∑ b : β, v a b ^ 2)

Cauchy--Schwarz for a double sum, in the shape the steps use: each term is dominated by a product, and the two factors separate.

Weighted sums

theorem MIPRE.sum_weighted_add {ι : Type u_1} [Fintype ι] (w f g : ι → ℝ) : ∑ i : ι, w i * (f i + g i) = ∑ i : ι, w i * f i + ∑ i : ι, w i * g i

theorem MIPRE.sum_weighted_const_mul {ι : Type u_1} [Fintype ι] (c : ℝ) (w f : ι → ℝ) : ∑ i : ι, w i * (c * f i) = c * ∑ i : ι, w i * f i

theorem MIPRE.sum_weighted_div {ι : Type u_1} [Fintype ι] (w f : ι → ℝ) (c : ℝ) : ∑ i : ι, w i * (f i / c) = (∑ i : ι, w i * f i) / c

The pasted family, and sandwiches of projective measurements in a ⋆-ring

The algebra of the pasting sandwich uses only that the families are projective measurements, so it is stated in any ⋆-ring (MIPRE/Foundations/Measurement.lean): a player's algebra, or a matrix algebra. Unlike sand of MIPRE/Foundations/Sandwich.lean, the two families here have different outcome sets.

def MIPRE.pasteJ {S : Type u_1} {R1 : Type u_2} {R2 : Type u_3} {K : Type u_4} [NonUnitalNonAssocSemiring S] [DecidableEq R2] [Fintype K] (R : R1 → S) (G : K → S) (e : K → R2) (p : R1 × R2) : S

The pasted POVM: the paper's J_{[eval = (a_1, a_2)]}. R is already the coarse-graining of the paper's G_1 along its own outcome map --- only R's projectivity is used, so it enters as a single projective family, and the inner coarse-graining is the consumer's business. It is defined in any semiring, so that the two families may be matrices or elements of the second player's algebra.

Equations

• MIPRE.pasteJ R G e p = ∑ g : K with e g = p.2, G g * R p.1 * G g

theorem MIPRE.IsPVMIn.sum_star_mul_self {S : Type u_1} [Ring S] [StarRing S] {A : Type u_2} [Fintype A] {X : A → S} (hX : IsPVMIn X) : ∑ a : A, star (X a) * X a = 1

The elements of a projective measurement satisfy ∑ P* P = 1.

theorem MIPRE.IsPVMIn.comp_equiv {S : Type u_1} [Ring S] [StarRing S] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] {X : A → S} (hX : IsPVMIn X) (e : B ≃ A) : IsPVMIn fun (b : B) => X (e b)

A projective measurement stays projective under a relabelling of its outcomes by a bijection.

theorem MIPRE.IsPVMIn.conj_eq_gram {S : Type u_1} [Ring S] [StarRing S] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] {X : A → S} {Z : B → S} (hX : IsPVMIn X) (hZ : IsPVMIn Z) (a : A) (b : B) : Z b * X a * Z b = star (X a * Z b) * (X a * Z b)

One projective measurement's element conjugated by another's is a Gram element: Z_b X_a Z_b = (X_a Z_b)* (X_a Z_b), the two families on any outcome sets. This is where the positivity of both pasting sandwiches comes from.

theorem MIPRE.IsPVMIn.sum_conj {S : Type u_1} [Ring S] [StarRing S] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] {X : A → S} {Z : B → S} (hX : IsPVMIn X) (hZ : IsPVMIn Z) : ∑ p : A × B, Z p.2 * X p.1 * Z p.2 = 1

The conjugates Z_b X_a Z_b sum to one, the conjugating index second: the inner family sums away against the outer one's projectivity.

theorem MIPRE.IsPVMIn.sum_conj' {S : Type u_1} [Ring S] [StarRing S] {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] {X : A → S} {Z : B → S} (hX : IsPVMIn X) (hZ : IsPVMIn Z) : ∑ p : B × A, Z p.1 * X p.2 * Z p.1 = 1

The conjugates Z_b X_a Z_b sum to one, the conjugating index first.

theorem MIPRE.IsPVMIn.sum_pasteJ {S : Type u_1} [Ring S] [StarRing S] {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [Fintype R2] [DecidableEq R2] [Fintype K] {R : R1 → S} {G : K → S} (hR : IsPVMIn R) (hG : IsPVMIn G) (e : K → R2) : ∑ p : R1 × R2, pasteJ R G e p = 1

The pasted family sums to one.

theorem MIPRE.IsPVMIn.pasteJ_nonneg {S : Type u_1} [Ring S] [StarRing S] {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [Fintype R2] [DecidableEq R2] [Fintype K] {R : R1 → S} {G : K → S} [PartialOrder S] [StarOrderedRing S] (hR : IsPVMIn R) (hG : IsPVMIn G) (e : K → R2) (p : R1 × R2) : 0 ≤ pasteJ R G e p

The pasted family is a POVM in a star-ordered ring: each of its terms is a Gram element.

Positive contractions

theorem MIPRE.sum_mul_self_le_one_of_sum_le_one {A : Type u_1} [Ring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [TopologicalSpace A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {C : Type u_2} [Fintype C] {P : C → A} (hP0 : ∀ (c : C), 0 ≤ P c) (hPsum : ∑ c : C, P c ≤ 1) : ∑ c : C, P c * P c ≤ 1

A family of positive elements summing to at most one has its squares summing to at most one, in any ordered algebra with a continuous functional calculus --- the matrices and the operators on a Hilbert space alike: P² ≤ P for each, because P (1 - P) is a product of commuting positive elements.

In a model

The estimates are proved once. Those about a single represented algebra --- NW19's Fact 4.31, the two mass bounds, the commutator expansion --- are stated for a state model (MIPRE/Foundations/StateModel.lean); the pasting argument itself for a bipartite model, with the first player's joint measurement A and copy Ga of G in 𝒜, and the second player's families R and G in ℬ. The matrix statements further down are the instances in the tensor-product model.

theorem MIPRE.StateModel.qform_star {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (T : 𝒞) : M.qform (star T) = M.qform T

The quadratic form does not see the adjoint: it is a real part, and the adjoint conjugates.

theorem MIPRE.StateModel.π_star_mul_self_nonneg {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (x : 𝒞) : 0 ≤ M.π (star x * x)

A Gram element is represented by a positive operator.

theorem MIPRE.StateModel.snorm_sq_le_qform {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h0 : 0 ≤ M.π T) (h1 : M.π T ≤ 1) : M.snorm T ^ 2 ≤ M.qform T

An element represented between 0 and 1 has ‖π T ψ‖² ≤ ⟨ψ, π T ψ⟩, because t² ≤ t there.

theorem MIPRE.StateModel.qform_mul_self_le {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {T : 𝒞} (h0 : 0 ≤ M.π T) (h1 : M.π T ≤ 1) : M.qform (T * T) ≤ M.qform T

An element represented between 0 and 1 has ⟨ψ, π(T²) ψ⟩ ≤ ⟨ψ, π T ψ⟩.

Two ways for a family of squared state norms to sum to at most one

theorem MIPRE.StateModel.sum_snorm_sq_orth_le_one {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) {ι : Type u_2} [Fintype ι] [DecidableEq ι] (P : ι → 𝒞) (hsa : ∀ (i : ι), star (P i) = P i) (hidem : ∀ (i : ι), P i * P i = P i) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) : ∑ i : ι, M.snorm (P i) ^ 2 ≤ 1

Mutually orthogonal projections: the sum is a projection, hence a contraction.

theorem MIPRE.StateModel.sum_snorm_sq_povm_le_one {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) {ι : Type u_2} [Fintype ι] {P : ι → 𝒞} (hP0 : ∀ (i : ι), 0 ≤ M.π (P i)) (hPsum : ∑ i : ι, M.π (P i) ≤ 1) : ∑ i : ι, M.snorm (P i) ^ 2 ≤ 1

A POVM, positive on the Hilbert space: each square is below the element, and the elements sum to at most the identity.

A sub-measurement close to a projective measurement

theorem MIPRE.StateModel.qform_sum_ge_of_close {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) {C : Type u_2} [Fintype C] {Q P : C → 𝒞} (hQ : IsPVMIn Q) (hP0 : ∀ (c : C), 0 ≤ M.π (P c)) (hPsum : ∑ c : C, M.π (P c) ≤ 1) {δ : ℝ} (hclose : ∑ c : C, M.snorm (Q c - P c) ^ 2 ≤ δ) : 1 - 2 * √δ ≤ ∑ c : C, M.qform (P c)

NW19's Fact 4.31. A family represented by positive operators summing to at most the identity, which is delta-close to a projective measurement on the state, carries all but 2 sqrt(delta) of the mass. Two Cauchy--Schwarz steps against the same deviation: one moves from 1 to sum <Q_c P_c>, the other from there to sum <P_c^2>, and P_c^2 <= P_c on the Hilbert space.

theorem MIPRE.StateModel.sum_snorm_sq_cool_prod {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) {R1 : Type u_2} {R2 : Type u_3} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {A : R1 × R2 → 𝒞} (hA : IsPVMIn A) (B : R1 × R2 → 𝒞) : ∑ a : R1, M.snorm (∑ b : R2, (A (a, b) - A (a, b) * B (a, b))) ^ 2 ≤ ∑ p : R1 × R2, M.snorm (A p - B p) ^ 2

sum_snorm_sq_cool at the fibres of the first projection of a product outcome set.

theorem MIPRE.StateModel.sum_snorm_sq_comm_eq {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (hψ : ‖M.ψ‖ = 1) {R1 : Type u_2} {G2 : Type u_3} [Fintype R1] [Fintype G2] {A : R1 → 𝒞} {B : G2 → 𝒞} (hA : IsPVMIn A) (hB : IsPVMIn B) : ∑ a : R1, ∑ g : G2, M.snorm (A a * B g - B g * A a) ^ 2 = 2 - 2 * ∑ a : R1, ∑ g : G2, M.qform (A a * B g * A a * B g)

The commutator sum of two projective families, as the deficit of one overlap. Both the fine-grained and the coarse-grained commutators of the pasting lemma have this shape, and it is what lets them be compared.

Born probabilities of projections

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

theorem MIPRE.BipartiteModel.snorm_sq_πA_mul_πB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {p : 𝒜} (hp : IsStarProjection p) (y : ℬ) : M.snorm (M.πA p * M.πB y) ^ 2 = M.bornProb p (star y * y)

A projection of the first player against a Gram element of the second: the Born probability is the squared norm of a product.

theorem MIPRE.BipartiteModel.bornProb_gram_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {p : 𝒜} (hp : IsStarProjection p) (y : ℬ) : 0 ≤ M.bornProb p (star y * y)

theorem MIPRE.BipartiteModel.snorm_sq_prod_proj {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {p : 𝒜} {q : ℬ} (hp : IsStarProjection p) (hq : IsStarProjection q) : M.snorm (M.πA p * M.πB q) ^ 2 = M.bornProb p q

A product of two commuting projections is a projection, so its squared state norm is its quadratic form --- a Born probability.

theorem MIPRE.BipartiteModel.bornProb_proj_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {p : 𝒜} {q : ℬ} (hp : IsStarProjection p) (hq : IsStarProjection q) : 0 ≤ M.bornProb p q

Coarse-graining a pair of projective families, on the two players

theorem MIPRE.BipartiteModel.sum_bornProb_le_fibSum {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] [DecidableEq β] {X : α → 𝒜} {X' : α → ℬ} (hX : IsPVMIn X) (hX' : IsPVMIn X') (e : α → β) : ∑ a : α, M.bornProb (X a) (X' a) ≤ ∑ b : β, M.bornProb (fibSumIn X e b) (fibSumIn X' e b)

Coarse-graining adds the off-diagonal Born probabilities, which are nonnegative.

theorem MIPRE.BipartiteModel.sum_xSqNorm_fibSum_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] [DecidableEq β] (hψ : ‖M.ψ‖ = 1) {X : α → 𝒜} {X' : α → ℬ} (hX : IsPVMIn X) (hX' : IsPVMIn X') (e : α → β) : ∑ b : β, M.xSqNorm (fibSumIn X e b) (fibSumIn X' e b) ≤ ∑ a : α, M.xSqNorm (X a) (X' a)

Coarse-graining two projective families the same way costs nothing, in the fibSumIn form that the pasting lemma needs.

theorem MIPRE.BipartiteModel.sum_snorm_sq_comm_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) {R1 : Type u_4} {G2 : Type u_5} [Fintype R1] [Fintype G2] {A : R1 → ℬ} {B : G2 → ℬ} (hA : IsPVMIn A) (hB : IsPVMIn B) : ∑ a : R1, ∑ g : G2, M.swap.stateSqNorm (A a * B g - B g * A a) = 2 - 2 * ∑ a : R1, ∑ g : G2, M.qform (M.πB (A a * B g * A a * B g))

The commutator sum of two projective families of the second player, as the deficit of one overlap.

The sandwich family of the pasting lemma

theorem MIPRE.BipartiteModel.sum_snorm_sq_sandOp_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) (hR : IsPVMIn R) (hG : IsPVMIn G) : ∑ a : R1, ∑ g : K, M.swap.stateSqNorm (R a * G g * R a) ≤ 1

The squared state norms of the pasting sandwich sum to at most one: it is a POVM of Gram elements, positive on the Hilbert space whatever the order of ℬ.

theorem MIPRE.BipartiteModel.abs_sigma_sub_cloud_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {Ga : K → 𝒜} (hR : IsPVMIn R) (hG : IsPVMIn G) : |∑ a : R1, ∑ g : K, M.qform (M.πB (R a * G g * R a * G g)) - ∑ a : R1, ∑ g : K, M.bornProb (Ga g) (R a * G g * R a)| ≤ √(∑ g : K, M.xSqNorm (Ga g) (G g))

The cloud step. Replacing the second player's outer factor by the first player's copy of it costs the square root of their cross-party deviation --- and nothing depending on the size of K, because one factor R a stays in front of the deviation, so the sum over a is absorbed rather than repeated.

theorem MIPRE.BipartiteModel.sum_snorm_sq_prod_le_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (hψ : ‖M.ψ‖ = 1) {ι : Type u_7} {κ : Type u_8} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (P : ι → κ → 𝒜) (Q : κ → ℬ) (hPsa : ∀ (i : ι) (k : κ), star (P i k) = P i k) (hPidem : ∀ (i : ι) (k : κ), P i k * P i k = P i k) (hPorth : ∀ (i j : ι) (k : κ), i ≠ j → P i k * P j k = 0) (hQ : IsPVMIn Q) : ∑ i : ι, ∑ k : κ, M.snorm (M.πA (P i k) * M.πB (Q k)) ^ 2 ≤ 1

A mutually orthogonal family of products of commuting projections has its squared state norms summing to at most one. The first player's factor need not be a measurement in its own right: only self-adjointness, idempotence and orthogonality along the first index are used.

theorem MIPRE.BipartiteModel.abs_sand_sub_ord_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {A : R1 × R2 → 𝒜} (hA : IsPVMIn A) (hG : IsPVMIn G) (e : K → R2) : |∑ a : R1, ∑ g : K, M.bornProb (A (a, e g)) (G g * R a * G g) - ∑ a : R1, ∑ g : K, M.bornProb (A (a, e g)) (G g * R a)| ≤ √(∑ a : R1, ∑ g : K, M.swap.stateSqNorm (R a * G g - G g * R a))

From the sandwich to the ordered product. The difference is the first player's operator against the second player's commutator; the first player's projection times the second's is a mutually orthogonal family, so the Cauchy--Schwarz costs only the commutator.

theorem MIPRE.BipartiteModel.sum_bornProb_ord_ge {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {A : R1 × R2 → 𝒜} (hA : IsPVMIn A) (hR : IsPVMIn R) (hG : IsPVMIn G) (e : K → R2) : 1 - (∑ b : R2, M.xSqNorm (∑ a : R1, A (a, b)) (fibSumIn G e b)) / 2 - √((∑ a : R1, M.xSqNorm (∑ b : R2, A (a, b)) (R a)) / 2) ≤ ∑ a : R1, ∑ g : K, M.bornProb (A (a, e g)) (G g * R a)

Step (i) of the pasting lemma. The second player's two projections in the order G_g R_a, paired with the first player's joint outcome, already agree with the state at 1 - delta/2 - sqrt(delta/2): the outer factor sums away against the first player's marginal, and what is left is the R-consistency, whose square root is the only one in the whole argument that is not a commutator.

theorem MIPRE.BipartiteModel.sum_xSqNorm_pasteJ_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {A : R1 × R2 → 𝒜} (hA : IsPVMIn A) (hR : IsPVMIn R) (hG : IsPVMIn G) (e : K → R2) : ∑ p : R1 × R2, M.xSqNorm (A p) (pasteJ R G e p) ≤ 2 * (1 - ∑ p : R1 × R2, M.bornProb (A p) (pasteJ R G e p))

From the Born rule to the state-dependent distance: the first player's family is projective and the pasted family a POVM positive on the Hilbert space, so the summed deviation is at most twice the disagreement.

theorem MIPRE.BipartiteModel.sum_snorm_sq_comm_coarse_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {R : R1 → ℬ} {A : R1 × R2 → 𝒜} {Gf : R2 → ℬ} (hA : IsPVMIn A) (hR : IsPVMIn R) (hGf : IsPVMIn Gf) {δ₁ δ₂ : ℝ} (h1 : ∑ a : R1, M.xSqNorm (∑ b : R2, A (a, b)) (R a) ≤ δ₁) (h2 : ∑ b : R2, M.xSqNorm (∑ a : R1, A (a, b)) (Gf b) ≤ δ₂) : ∑ a : R1, ∑ b : R2, M.swap.stateSqNorm (R a * Gf b - Gf b * R a) ≤ 16 * (δ₁ + δ₂)

The coarse-grained commutator is small: this is the commutation analysis, with both families on the second player's side and the first player's joint measurement supplying the operator both products reach.

def MIPRE.BipartiteModel.collisionTerm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R2] [Fintype K] [DecidableEq K] (R : R1 → ℬ) (G : K → ℬ) (Ga : K → 𝒜) (e : K → R2) : ℝ

The collision term: the pairs of G-outcomes that the outcome map cannot tell apart. It is exactly what the coarse-grained cloud has beyond the fine-grained one, and the only place where the separating property of the outcome map is needed.

Equations

• M.collisionTerm R G Ga e = ∑ a : R1, ∑ g : K, ∑ g' : K with g' ≠ g ∧ e g' = e g, M.bornProb (Ga g') (R a * G g * R a)

theorem MIPRE.BipartiteModel.collisionTerm_nonneg {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} {Ga : K → 𝒜} (hR : IsPVMIn R) (hG : IsPVMIn G) (hGa : IsPVMIn Ga) (e : K → R2) : 0 ≤ M.collisionTerm R G Ga e

theorem MIPRE.BipartiteModel.strife_sub_cloud_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} {Ga : K → 𝒜} (e : K → R2) : ∑ a : R1, ∑ b : R2, M.bornProb (fibSumIn Ga e b) (R a * fibSumIn G e b * R a) - ∑ a : R1, ∑ g : K, M.bornProb (Ga g) (R a * G g * R a) = M.collisionTerm R G Ga e

The strife minus the cloud is exactly the collision term. Both are sums of the same Born probabilities; coarse-graining pairs each G-outcome with every other one the map identifies with it.

theorem MIPRE.BipartiteModel.sum_snorm_sq_comm_fine_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {A : R1 × R2 → 𝒜} {Ga : K → 𝒜} (hA : IsPVMIn A) (hR : IsPVMIn R) (hG : IsPVMIn G) (hGa : IsPVMIn Ga) (e : K → R2) {δ₁ δ₂ : ℝ} (h1 : ∑ a : R1, M.xSqNorm (∑ b : R2, A (a, b)) (R a) ≤ δ₁) (h2 : ∑ b : R2, M.xSqNorm (∑ a : R1, A (a, b)) (fibSumIn G e b) ≤ δ₂) : ∑ a : R1, ∑ g : K, M.swap.stateSqNorm (R a * G g - G g * R a) ≤ 16 * (δ₁ + δ₂) + 4 * √(∑ g : K, M.xSqNorm (Ga g) (G g)) + 2 * M.collisionTerm R G Ga e

The fine-grained commutator against the coarse-grained one. The coarse-grained one is small by the commutation analysis; the two differ by the cloud, the strife and the collision term, and the cloud--strife comparison is the only place the first player's copy of G is used.

theorem MIPRE.BipartiteModel.one_sub_sum_bornProb_pasteJ_le' {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → ℬ} {G : K → ℬ} (hψ : ‖M.ψ‖ = 1) {A : R1 × R2 → 𝒜} (hA : IsPVMIn A) (hR : IsPVMIn R) (hG : IsPVMIn G) (e : K → R2) : 1 - ∑ p : R1 × R2, M.bornProb (A p) (pasteJ R G e p) ≤ (∑ b : R2, M.xSqNorm (∑ a : R1, A (a, b)) (fibSumIn G e b)) / 2 + √((∑ a : R1, M.xSqNorm (∑ b : R2, A (a, b)) (R a)) / 2) + √(∑ a : R1, ∑ g : K, M.swap.stateSqNorm (R a * G g - G g * R a))

The pasted POVM agrees with the first player's joint measurement, at one question. Step (i) reaches the ordered product and step (ii) the sandwich.

The marginal of a joint measurement against the other player's product

theorem MIPRE.BipartiteModel.sum_xSqNorm_marg_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {Q : R1 × R2 → 𝒜} {Z : R2 → ℬ} (X : R1 → ℬ) (hQ : IsPVMIn Q) (hZ : IsPVMIn Z) : ∑ a : R1, M.xSqNorm (∑ b : R2, Q (a, b)) (X a) ≤ 2 * ∑ p : R1 × R2, M.snorm (M.πA (Q p) * M.πB (Z p.2) - M.πA (Q p)) ^ 2 + 2 * ∑ p : R1 × R2, M.xSqNorm (Q p) (Z p.2 * X p.1)

The marginal step. The first player's joint projective measurement, consistent with the second player's ordered product Z_b X_a, has its R2-marginal consistent with X_a alone.

theorem MIPRE.BipartiteModel.swap_stateSqNorm_sub_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (a : 𝒜) (b₁ b₂ : ℬ) : M.swap.stateSqNorm (b₁ - b₂) ≤ 2 * M.xSqNorm a b₁ + 2 * M.xSqNorm a b₂

The second player's own deviation, through the first player's operator. The three-term triangle inequality in the one shape the consumer needs: a same-side deviation bounded by two cross-party ones.

theorem MIPRE.BipartiteModel.sum_snorm_sq_mul_proj_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] (Q : R1 × R2 → 𝒜) {Z : R2 → ℬ} (X : R1 → ℬ) (hZ : IsPVMIn Z) : ∑ p : R1 × R2, M.snorm (M.πA (Q p) * M.πB (Z p.2) - M.πA (Q p)) ^ 2 ≤ 4 * ∑ p : R1 × R2, M.xSqNorm (Q p) (Z p.2 * X p.1)

Attaching the other player's projection to a consistent joint measurement costs nothing.

theorem MIPRE.BipartiteModel.sum_xSqNorm_marg_le' {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {R1 : Type u_4} {R2 : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {Q : R1 × R2 → 𝒜} {Z : R2 → ℬ} (X : R1 → ℬ) (hQ : IsPVMIn Q) (hZ : IsPVMIn Z) : ∑ a : R1, M.xSqNorm (∑ b : R2, Q (a, b)) (X a) ≤ 10 * ∑ p : R1 × R2, M.xSqNorm (Q p) (Z p.2 * X p.1)

The marginal step, packaged, at ten times the input.

The pasting lemma

theorem MIPRE.BipartiteModel.one_sub_sum_bornProb_pasteJ_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {ι : Type u_4} {R1 : Type u_5} {R2 : Type u_6} {K : Type u_7} [Fintype ι] [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] (hψ : ‖M.ψ‖ = 1) {w : ι → ℝ} (hw0 : ∀ (i : ι), 0 ≤ w i) (hw1 : ∑ i : ι, w i = 1) {A : ι → R1 × R2 → 𝒜} {R : ι → R1 → ℬ} {G : ι → K → ℬ} {Ga : ι → K → 𝒜} (e : ι → K → R2) (hA : ∀ (i : ι), IsPVMIn (A i)) (hR : ∀ (i : ι), IsPVMIn (R i)) (hG : ∀ (i : ι), IsPVMIn (G i)) (hGa : ∀ (i : ι), IsPVMIn (Ga i)) {δ η ε : ℝ} (hP1 : ∑ i : ι, w i * ∑ a : R1, M.xSqNorm (∑ b : R2, A i (a, b)) (R i a) ≤ δ) (hP2 : ∑ i : ι, w i * ∑ b : R2, M.xSqNorm (∑ a : R1, A i (a, b)) (fibSumIn (G i) (e i) b) ≤ δ) (hP4 : ∑ i : ι, w i * ∑ g : K, M.xSqNorm (Ga i g) (G i g) ≤ η) (hcoll : ∑ i : ι, w i * M.collisionTerm (R i) (G i) (Ga i) (e i) ≤ ε) : 1 - ∑ i : ι, w i * ∑ p : R1 × R2, M.bornProb (A i p) (pasteJ (R i) (G i) (e i) p) ≤ δ / 2 + √(δ / 2) + √(32 * δ + 4 * √η + 2 * ε)

The pasting lemma, k = 2 (NW19's Fact 4.35, the paper's lem:pasting-updated), in a bipartite model: the first player's joint measurement agrees with the pasted sandwich up to delta/2 + sqrt(delta/2) + sqrt(32 delta + 4 sqrt(eta) + 2 eps).

The collision term under a product question distribution

theorem MIPRE.BipartiteModel.sum_collisionTerm_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Z : Type u_4} {Y : Type u_5} {R1 : Type u_6} {R2 : Type u_7} {K : Type u_8} [Fintype Z] [DecidableEq Z] [Fintype Y] [DecidableEq Y] [Nonempty Y] [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] (hψ : ‖M.ψ‖ = 1) {ν : Z → ℝ} (hν0 : ∀ (z : Z), 0 ≤ ν z) {R : Z → R1 → ℬ} {G : Z → K → ℬ} {Ga : Z → K → 𝒜} (hR : ∀ (z : Z), IsPVMIn (R z)) (hG : ∀ (z : Z), IsPVMIn (G z)) (hGa : ∀ (z : Z), IsPVMIn (Ga z)) (e : Z → Y → K → R2) {εz : Z → ℝ} (hε : ∀ (z : Z), 0 ≤ εz z) (hsep : ∀ (z : Z) (g g' : K), g' ≠ g → ↑{y : Y | e z y g' = e z y g}.card ≤ εz z * ↑(Fintype.card Y)) : ∑ i : Z × Y, ν i.1 * (↑(Fintype.card Y))⁻¹ * M.collisionTerm (R i.1) (G i.1) (Ga i.1) (e i.1 i.2) ≤ ∑ z : Z, ν z * εz z

The collision term is at most the average collision probability, in a bipartite model: the Born probabilities do not depend on the probe, so the probe average acts on the indicator alone, and what is left is a POVM's total mass, which is one.

Two small facts about the quadratic form

theorem MIPRE.qform_conjTranspose {N : Type u_1} [Fintype N] [DecidableEq N] (v : N → ℂ) (M : Matrix N N ℂ) : qform v M.conjTranspose = qform v M

The quadratic form does not see the adjoint: it is a real part, and the adjoint conjugates.

theorem MIPRE.sum_sq_le_one_of_sum_eq_one {N : Type u_1} [Fintype N] [DecidableEq N] {C : Type u_2} [Fintype C] {P : C → Matrix N N ℂ} (hP0 : ∀ (c : C), 0 ≤ P c) (hPsum : ∑ c : C, P c = 1) : ∑ c : C, P c * P c ≤ 1

A positive operator below the identity has M^2 <= M, so a family of positive operators summing to the identity has its squares summing to at most the identity.

A sub-measurement close to a projective measurement

Two ways for a family of squared state norms to sum to at most one

theorem MIPRE.sum_snorm_sq_orth_le_one {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {v : N → ℂ} (hv : ‖evec v‖ = 1) (P : ι → Matrix N N ℂ) (hsa : ∀ (i : ι), (P i).conjTranspose = P i) (hidem : ∀ (i : ι), P i * P i = P i) (horth : ∀ (i j : ι), i ≠ j → P i * P j = 0) : ∑ i : ι, snorm v (P i) ^ 2 ≤ 1

Mutually orthogonal projections: the sum is a projection, hence bounded by the identity.

theorem MIPRE.sum_snorm_sq_povm_le_one {N : Type u_1} [Fintype N] [DecidableEq N] {ι : Type u_2} [Fintype ι] {v : N → ℂ} (hv : ‖evec v‖ = 1) {P : ι → Matrix N N ℂ} (hP0 : ∀ (i : ι), 0 ≤ P i) (hPsum : ∑ i : ι, P i = 1) : ∑ i : ι, snorm v (P i) ^ 2 ≤ 1

A POVM: each square is below the element, and the elements sum to the identity.

theorem MIPRE.aOp_zero {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] : aOp 0 = 0

theorem MIPRE.snorm_bOp_sq_eq_tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (Y : Matrix dB dB ℂ) : snorm ψ (bOp Y) ^ 2 = (BipartiteModel.tensor ψ).swap.stateSqNorm Y

Bob's squared state norm is the second player's in the tensor-product model.

theorem MIPRE.sum_aOp_conjTranspose_mul_self_of_isPVM {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} [Fintype ι] {P : ι → Matrix dA dA ℂ} (h : IsPVM P) : ∑ i : ι, (aOp (P i)).conjTranspose * aOp (P i) = 1

theorem MIPRE.bornProb_sum_left {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} (ψ : dA × dB → ℂ) (s : Finset ι) (A : ι → Matrix dA dA ℂ) (B : Matrix dB dB ℂ) : bornProb ψ (∑ i ∈ s, A i) B = ∑ i ∈ s, bornProb ψ (A i) B

theorem MIPRE.bornProb_sum_right {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} (ψ : dA × dB → ℂ) (s : Finset ι) (A : Matrix dA dA ℂ) (B : ι → Matrix dB dB ℂ) : bornProb ψ A (∑ i ∈ s, B i) = ∑ i ∈ s, bornProb ψ A (B i)

Coarse-graining a pair of projective families, on the two parties

theorem MIPRE.sum_bornProb_le_fibSum {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {α : Type u_3} {β : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ψ : dA × dB → ℂ) {X : α → Matrix dA dA ℂ} {X' : α → Matrix dB dB ℂ} (hX : IsPVM X) (hX' : IsPVM X') (e : α → β) : ∑ a : α, bornProb ψ (X a) (X' a) ≤ ∑ b : β, bornProb ψ (fibSum X e b) (fibSum X' e b)

Coarse-graining adds the off-diagonal Born probabilities, which are nonnegative.

theorem MIPRE.sum_xSqNorm_fibSum_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {α : Type u_3} {β : Type u_4} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {X : α → Matrix dA dA ℂ} {X' : α → Matrix dB dB ℂ} (hX : IsPVM X) (hX' : IsPVM X') (e : α → β) : ∑ b : β, xSqNorm ψ (fibSum X e b) (fibSum X' e b) ≤ ∑ a : α, xSqNorm ψ (X a) (X' a)

Coarse-graining two projective families the same way costs nothing, in the fibSum form that the pasting lemma needs.

The fine-grained commutator against the coarse-grained one

theorem MIPRE.sum_snorm_sq_comm_eq {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {G2 : Type u_5} {R1 : Type u_6} [Fintype G2] [DecidableEq G2] [Fintype R1] [DecidableEq R1] {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 → Matrix dB dB ℂ} {B : G2 → Matrix dB dB ℂ} (hA : IsPVM A) (hB : IsPVM B) : ∑ a : R1, ∑ g : G2, snorm ψ (bOp (A a * B g - B g * A a)) ^ 2 = 2 - 2 * ∑ a : R1, ∑ g : G2, qform ψ (bOp (A a * B g * A a * B g))

The commutator sum of two projective families on Bob's factor, written as the deficit of one overlap. Both the fine-grained and the coarse-grained commutators have this shape, and it is what lets them be compared.

The sandwich family of the pasting lemma

theorem MIPRE.sandOp_posSemidef {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) (a : R1) (g : K) : (R a * G g * R a).PosSemidef

Each term of the pasting sandwich is a Gram operator, hence positive.

theorem MIPRE.sum_sandOp {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) : ∑ p : R1 × K, R p.1 * G p.2 * R p.1 = 1

The pasting sandwich is a POVM: the inner family sums away against R's projectivity.

theorem MIPRE.sum_snorm_sq_sandOp_le_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) (hR : IsPVM R) (hG : IsPVM G) : ∑ a : R1, ∑ g : K, snorm ψ (bOp (R a * G g * R a)) ^ 2 ≤ 1

The squared state norms of the pasting sandwich sum to at most one.

theorem MIPRE.abs_sigma_sub_cloud_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {Ga : K → Matrix dA dA ℂ} (hR : IsPVM R) (hG : IsPVM G) : |∑ a : R1, ∑ g : K, qform ψ (bOp (R a * G g * R a * G g)) - ∑ a : R1, ∑ g : K, bornProb ψ (Ga g) (R a * G g * R a)| ≤ √(∑ g : K, xSqNorm ψ (Ga g) (G g))

The cloud step. Replacing Bob's outer factor by Alice's copy of it costs the square root of their cross-party deviation --- and nothing depending on the size of K, because one factor R a stays in front of the deviation, so the sum over a is absorbed rather than repeated.

Alice's operator against Bob's projection

theorem MIPRE.sum_snorm_sq_prod_le_one {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_6} {κ : Type u_7} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) (P : ι → κ → Matrix dA dA ℂ) (Q : κ → Matrix dB dB ℂ) (hPsa : ∀ (i : ι) (k : κ), (P i k).conjTranspose = P i k) (hPidem : ∀ (i : ι) (k : κ), P i k * P i k = P i k) (hPorth : ∀ (i j : ι) (k : κ), i ≠ j → P i k * P j k = 0) (hQ : IsPVM Q) : ∑ i : ι, ∑ k : κ, snorm ψ (aOp (P i k) * bOp (Q k)) ^ 2 ≤ 1

A mutually orthogonal family of products of commuting projections has its squared state norms summing to at most one. Alice's factor need not be a measurement in its own right: only self-adjointness, idempotence and orthogonality along the first index are used.

theorem MIPRE.abs_sand_sub_ord_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 × R2 → Matrix dA dA ℂ} (hA : IsPVM A) (hG : IsPVM G) (e : K → R2) : |∑ a : R1, ∑ g : K, bornProb ψ (A (a, e g)) (G g * R a * G g) - ∑ a : R1, ∑ g : K, bornProb ψ (A (a, e g)) (G g * R a)| ≤ √(∑ a : R1, ∑ g : K, snorm ψ (bOp (R a * G g - G g * R a)) ^ 2)

From the sandwich to the ordered product. The difference is Alice's operator against Bob's commutator; Alice's projection times Bob's is a mutually orthogonal family, so the Cauchy--Schwarz costs only the commutator.

The ordered product carries almost all the mass

theorem MIPRE.sum_bornProb_ord_ge {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 × R2 → Matrix dA dA ℂ} (hA : IsPVM A) (hR : IsPVM R) (hG : IsPVM G) (e : K → R2) : 1 - (∑ b : R2, xSqNorm ψ (∑ a : R1, A (a, b)) (fibSum G e b)) / 2 - √((∑ a : R1, xSqNorm ψ (∑ b : R2, A (a, b)) (R a)) / 2) ≤ ∑ a : R1, ∑ g : K, bornProb ψ (A (a, e g)) (G g * R a)

Step (i) of the pasting lemma. Bob's two projections in the order G_g R_a, paired with Alice's joint outcome, already agree with the state at 1 - delta/2 - sqrt(delta/2): the outer factor sums away against Alice's marginal, and what is left is the R-consistency, whose square root is the only one in the whole argument that is not a commutator.

The pasted POVM

theorem MIPRE.sandOpG_posSemidef {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) (a : R1) (g : K) : (G g * R a * G g).PosSemidef

The other sandwich --- the one the pasted POVM is built from --- is also a Gram operator.

theorem MIPRE.sum_sandOpG {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) : ∑ p : R1 × K, G p.2 * R p.1 * G p.2 = 1

theorem MIPRE.pasteJ_posSemidef {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) (e : K → R2) (p : R1 × R2) : (pasteJ R G e p).PosSemidef

theorem MIPRE.sum_pasteJ {dB : Type u_2} [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (hR : IsPVM R) (hG : IsPVM G) (e : K → R2) : ∑ p : R1 × R2, pasteJ R G e p = 1

theorem MIPRE.sum_xSqNorm_pasteJ_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 × R2 → Matrix dA dA ℂ} (hA : IsPVM A) (hR : IsPVM R) (hG : IsPVM G) (e : K → R2) : ∑ p : R1 × R2, xSqNorm ψ (A p) (pasteJ R G e p) ≤ 2 * (1 - ∑ p : R1 × R2, bornProb ψ (A p) (pasteJ R G e p))

From the Born rule to the state-dependent distance: Alice's family is projective and the pasted family is a POVM, so the summed deviation is at most twice the disagreement.

The coarse-grained commutator, and the collision term

theorem MIPRE.sum_snorm_sq_comm_coarse_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {R : R1 → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} {A : R1 × R2 → Matrix dA dA ℂ} {Gf : R2 → Matrix dB dB ℂ} (hA : IsPVM A) (hR : IsPVM R) (hGf : IsPVM Gf) {δ₁ δ₂ : ℝ} (h1 : ∑ a : R1, xSqNorm ψ (∑ b : R2, A (a, b)) (R a) ≤ δ₁) (h2 : ∑ b : R2, xSqNorm ψ (∑ a : R1, A (a, b)) (Gf b) ≤ δ₂) : ∑ a : R1, ∑ b : R2, snorm ψ (bOp (R a * Gf b - Gf b * R a)) ^ 2 ≤ 16 * (δ₁ + δ₂)

The coarse-grained commutator is small: this is the commutation analysis, with both families on Bob's factor and Alice's joint measurement supplying the operator both products reach.

def MIPRE.collisionTerm {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R2] [Fintype K] [DecidableEq K] (ψ : dA × dB → ℂ) (R : R1 → Matrix dB dB ℂ) (G : K → Matrix dB dB ℂ) (Ga : K → Matrix dA dA ℂ) (e : K → R2) : ℝ

The collision term: the pairs of G-outcomes that the outcome map cannot tell apart. It is exactly what the coarse-grained cloud has beyond the fine-grained one, and the only place where the separating property of the outcome map is needed.

Equations

• MIPRE.collisionTerm ψ R G Ga e = ∑ a : R1, ∑ g : K, ∑ g' : K with g' ≠ g ∧ e g' = e g, MIPRE.bornProb ψ (Ga g') (R a * G g * R a)

theorem MIPRE.collisionTerm_eq_tensor {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] (ψ : dA × dB → ℂ) (R : R1 → Matrix dB dB ℂ) (G : K → Matrix dB dB ℂ) (Ga : K → Matrix dA dA ℂ) (e : K → R2) : collisionTerm ψ R G Ga e = (BipartiteModel.tensor ψ).collisionTerm R G Ga e

The collision term is that of the tensor-product model.

theorem MIPRE.collisionTerm_nonneg {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} (ψ : dA × dB → ℂ) {Ga : K → Matrix dA dA ℂ} (hR : IsPVM R) (hG : IsPVM G) (hGa : IsPVM Ga) (e : K → R2) : 0 ≤ collisionTerm ψ R G Ga e

theorem MIPRE.strife_sub_cloud_eq {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} {Ga : K → Matrix dA dA ℂ} (e : K → R2) : ∑ a : R1, ∑ b : R2, bornProb ψ (fibSum Ga e b) (R a * fibSum G e b * R a) - ∑ a : R1, ∑ g : K, bornProb ψ (Ga g) (R a * G g * R a) = collisionTerm ψ R G Ga e

The strife minus the cloud is exactly the collision term. Both are sums of the same Born probabilities; coarse-graining pairs each G-outcome with every other one the map identifies with it.

The two halves of the pasting lemma, at one question

theorem MIPRE.sum_snorm_sq_comm_fine_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 × R2 → Matrix dA dA ℂ} {Ga : K → Matrix dA dA ℂ} (hA : IsPVM A) (hR : IsPVM R) (hG : IsPVM G) (hGa : IsPVM Ga) (e : K → R2) {δ₁ δ₂ : ℝ} (h1 : ∑ a : R1, xSqNorm ψ (∑ b : R2, A (a, b)) (R a) ≤ δ₁) (h2 : ∑ b : R2, xSqNorm ψ (∑ a : R1, A (a, b)) (fibSum G e b) ≤ δ₂) : ∑ a : R1, ∑ g : K, snorm ψ (bOp (R a * G g - G g * R a)) ^ 2 ≤ 16 * (δ₁ + δ₂) + 4 * √(∑ g : K, xSqNorm ψ (Ga g) (G g)) + 2 * collisionTerm ψ R G Ga e

The fine-grained commutator against the coarse-grained one. The coarse-grained one is small by the commutation analysis; the two differ by the cloud, the strife and the collision term, and the cloud--strife comparison is the only place Alice's copy of G is used.

theorem MIPRE.one_sub_sum_bornProb_pasteJ_le' {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} {K : Type u_5} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {R : R1 → Matrix dB dB ℂ} {G : K → Matrix dB dB ℂ} {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {A : R1 × R2 → Matrix dA dA ℂ} (hA : IsPVM A) (hR : IsPVM R) (hG : IsPVM G) (e : K → R2) : 1 - ∑ p : R1 × R2, bornProb ψ (A p) (pasteJ R G e p) ≤ (∑ b : R2, xSqNorm ψ (∑ a : R1, A (a, b)) (fibSum G e b)) / 2 + √((∑ a : R1, xSqNorm ψ (∑ b : R2, A (a, b)) (R a)) / 2) + √(∑ a : R1, ∑ g : K, snorm ψ (bOp (R a * G g - G g * R a)) ^ 2)

The pasted POVM agrees with Alice's joint measurement, at one question. Step (i) reaches the ordered product and step (ii) the sandwich.

The marginal of a joint measurement against the other party's product

The step lem:qld-pairs-of-lines needs before the pasting lemma applies: a joint measurement consistent with the ordered product of the other party's two families is consistent, after summing out one outcome, with that party's single family. Two facts do it: sum_snorm_sq_cool, to replace the marginal by the same marginal with the other party's projection attached, and then the orthogonality of that projection's fibres, which is what makes the sum over the summed-out outcome free rather than a factor |R2|.

theorem MIPRE.IsPVM.aOp {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_5} [Fintype ι] {Q : ι → Matrix dA dA ℂ} (h : IsPVM Q) : IsPVM fun (i : ι) => MIPRE.aOp (Q i)

A projective family stays projective on the product space.

theorem MIPRE.IsPVM.bOp {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_5} [Fintype ι] {Q : ι → Matrix dB dB ℂ} (h : IsPVM Q) : IsPVM fun (i : ι) => MIPRE.bOp (Q i)

theorem MIPRE.sum_fibre_fst {ι : Type u_5} {κ : Type u_6} {M : Type u_7} [Fintype ι] [DecidableEq ι] [Fintype κ] [AddCommMonoid M] (i : ι) (g : ι × κ → M) : ∑ p : ι × κ with p.1 = i, g p = ∑ k : κ, g (i, k)

theorem MIPRE.sum_snorm_sq_cool_prod {R1 : Type u_3} {R2 : Type u_4} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {N : Type u_5} [Fintype N] [DecidableEq N] (v : N → ℂ) {A : R1 × R2 → Matrix N N ℂ} (hA : IsPVM A) (B : R1 × R2 → Matrix N N ℂ) : ∑ a : R1, snorm v (∑ b : R2, (A (a, b) - A (a, b) * B (a, b))) ^ 2 ≤ ∑ p : R1 × R2, snorm v (A p - B p) ^ 2

sum_snorm_sq_cool at the fibres of the first projection of a product outcome set.

theorem MIPRE.sum_xSqNorm_marg_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {ψ : dA × dB → ℂ} {Q : R1 × R2 → Matrix dA dA ℂ} {Z : R2 → Matrix dB dB ℂ} (X : R1 → Matrix dB dB ℂ) (hQ : IsPVM Q) (hZ : IsPVM Z) : ∑ a : R1, xSqNorm ψ (∑ b : R2, Q (a, b)) (X a) ≤ 2 * ∑ p : R1 × R2, snorm ψ (aOp (Q p) * bOp (Z p.2) - aOp (Q p)) ^ 2 + 2 * ∑ p : R1 × R2, xSqNorm ψ (Q p) (Z p.2 * X p.1)

The marginal step. Alice's joint projective measurement, consistent with Bob's ordered product Z_b X_a, has its R2-marginal consistent with X_a alone.

theorem MIPRE.IsPVM.comp_equiv {N : Type u_5} {ι : Type u_6} {κ : Type u_7} [Fintype N] [DecidableEq N] [Fintype ι] [Fintype κ] {P : ι → Matrix N N ℂ} (h : IsPVM P) (e : κ ≃ ι) : IsPVM fun (k : κ) => P (e k)

A projective family stays projective under a relabelling of its outcomes by a bijection.

theorem MIPRE.normSq_stateVecB_sub_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (ψ : dA × dB → ℂ) (A : Matrix dA dA ℂ) (B₁ B₂ : Matrix dB dB ℂ) : ‖stateVecB ψ (B₁ - B₂)‖ ^ 2 ≤ 2 * xSqNorm ψ A B₁ + 2 * xSqNorm ψ A B₂

Bob's own deviation, through Alice's operator. The three-term triangle inequality in the one shape the consumer needs: a same-side deviation bounded by two cross-party ones.

theorem MIPRE.sum_snorm_sq_mul_proj_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {ψ : dA × dB → ℂ} (Q : R1 × R2 → Matrix dA dA ℂ) {Z : R2 → Matrix dB dB ℂ} (X : R1 → Matrix dB dB ℂ) (hZ : IsPVM Z) : ∑ p : R1 × R2, snorm ψ (aOp (Q p) * bOp (Z p.2) - aOp (Q p)) ^ 2 ≤ 4 * ∑ p : R1 × R2, xSqNorm ψ (Q p) (Z p.2 * X p.1)

Attaching the other party's projection to a consistent joint measurement costs nothing. The relation the marginal step's first term needs, from the consistency with the ordered product alone.

theorem MIPRE.sum_xSqNorm_marg_le' {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {R1 : Type u_3} {R2 : Type u_4} [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] {ψ : dA × dB → ℂ} {Q : R1 × R2 → Matrix dA dA ℂ} {Z : R2 → Matrix dB dB ℂ} (X : R1 → Matrix dB dB ℂ) (hQ : IsPVM Q) (hZ : IsPVM Z) : ∑ a : R1, xSqNorm ψ (∑ b : R2, Q (a, b)) (X a) ≤ 10 * ∑ p : R1 × R2, xSqNorm ψ (Q p) (Z p.2 * X p.1)

The marginal step, packaged. A joint projective measurement consistent with the other party's ordered product Z_b X_a has its R2-marginal consistent with X_a alone, at ten times the input.

Transport to a twice-extended state

The consumer's two inputs live on different spaces: the joint measurement on each party's space enlarged by one register (the Naimark dilation of lem:qld-combined-points), the line measurements on the unenlarged ones. An operator with an inert ancilla has the same cross-party deviation on the extended state as the operator itself.

theorem MIPRE.xSqNorm_extVec2_aOp {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {Anc : Type u_3} {Bnc : Type u_4} [Fintype Anc] [DecidableEq Anc] [Fintype Bnc] [DecidableEq Bnc] (ψ : dA × dB → ℂ) (a₀ : Anc) (b₀ : Bnc) {P : Matrix dA dA ℂ} (hP : P.conjTranspose = P) (Q : Matrix dB dB ℂ) : xSqNorm (extVec2 ψ a₀ b₀) (aOp P) (aOp Q) = xSqNorm ψ P Q

The pasting lemma

The averaged statement. A is Alice's joint projective measurement, R Bob's first family --- in the application already the coarse-graining of his answer measurement along its own outcome map --- and G his second, with Ga Alice's copy of it. The four hypotheses are the two marginal consistencies, the cross-party self-consistency of G at the fine level, and the collision term.

Two hypotheses of the paper's statement are absent, and both are absences rather than gaps. G_1 is assumed projective (in the paper it may be a POVM for i = 1), which makes the two diagonal sums of the commutator expansion exactly one and removes the need for NW19's Fact 4.31. And the cross-party self-consistency of G is a hypothesis here rather than derived from the backwards consistency and Alice's self-consistency, because the consumer has it directly, at the fine level and with no collision cost.

theorem MIPRE.one_sub_sum_bornProb_pasteJ_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {ι : Type u_3} {R1 : Type u_4} {R2 : Type u_5} {K : Type u_6} [Fintype ι] [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {w : ι → ℝ} (hw0 : ∀ (i : ι), 0 ≤ w i) (hw1 : ∑ i : ι, w i = 1) {A : ι → R1 × R2 → Matrix dA dA ℂ} {R : ι → R1 → Matrix dB dB ℂ} {G : ι → K → Matrix dB dB ℂ} {Ga : ι → K → Matrix dA dA ℂ} (e : ι → K → R2) (hA : ∀ (i : ι), IsPVM (A i)) (hR : ∀ (i : ι), IsPVM (R i)) (hG : ∀ (i : ι), IsPVM (G i)) (hGa : ∀ (i : ι), IsPVM (Ga i)) {δ η ε : ℝ} (hP1 : ∑ i : ι, w i * ∑ a : R1, xSqNorm ψ (∑ b : R2, A i (a, b)) (R i a) ≤ δ) (hP2 : ∑ i : ι, w i * ∑ b : R2, xSqNorm ψ (∑ a : R1, A i (a, b)) (fibSum (G i) (e i) b) ≤ δ) (hP4 : ∑ i : ι, w i * ∑ g : K, xSqNorm ψ (Ga i g) (G i g) ≤ η) (hcoll : ∑ i : ι, w i * collisionTerm ψ (R i) (G i) (Ga i) (e i) ≤ ε) : 1 - ∑ i : ι, w i * ∑ p : R1 × R2, bornProb ψ (A i p) (pasteJ (R i) (G i) (e i) p) ≤ δ / 2 + √(δ / 2) + √(32 * δ + 4 * √η + 2 * ε)

The pasting lemma, k = 2 (NW19's Fact 4.35, the paper's lem:pasting-updated), in Born probability form: Alice's joint measurement agrees with the pasted sandwich up to delta/2 + sqrt(delta/2) + sqrt(32 delta + 4 sqrt(eta) + 2 eps).

The collision term under a product question distribution

theorem MIPRE.sum_collisionTerm_le {dA : Type u_1} {dB : Type u_2} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] {Z : Type u_3} {Y : Type u_4} {R1 : Type u_5} {R2 : Type u_6} {K : Type u_7} [Fintype Z] [DecidableEq Z] [Fintype Y] [DecidableEq Y] [Nonempty Y] [Fintype R1] [DecidableEq R1] [Fintype R2] [DecidableEq R2] [Fintype K] [DecidableEq K] {ψ : dA × dB → ℂ} (hψ : ‖evec ψ‖ = 1) {ν : Z → ℝ} (hν0 : ∀ (z : Z), 0 ≤ ν z) {R : Z → R1 → Matrix dB dB ℂ} {G : Z → K → Matrix dB dB ℂ} {Ga : Z → K → Matrix dA dA ℂ} (hR : ∀ (z : Z), IsPVM (R z)) (hG : ∀ (z : Z), IsPVM (G z)) (hGa : ∀ (z : Z), IsPVM (Ga z)) (e : Z → Y → K → R2) {εz : Z → ℝ} (hε : ∀ (z : Z), 0 ≤ εz z) (hsep : ∀ (z : Z) (g g' : K), g' ≠ g → ↑{y : Y | e z y g' = e z y g}.card ≤ εz z * ↑(Fintype.card Y)) : ∑ i : Z × Y, ν i.1 * (↑(Fintype.card Y))⁻¹ * collisionTerm ψ (R i.1) (G i.1) (Ga i.1) (e i.1 i.2) ≤ ∑ z : Z, ν z * εz z

The collision term is at most the average collision probability. The question is a pair: a part z that all the measurements see, and a probe y, uniform and independent of z, that only the outcome map sees. The Born probabilities do not depend on y, so the probe average acts on the indicator alone; what is left is a POVM's total mass, which is one.

The collision probability is allowed to depend on z, and the conclusion is its average. The consumer needs that: for a degenerate line the outcome map separates nothing, and what makes the average small is that such lines are rare rather than that the bound holds everywhere.