Preliminary comparison theorems: core layer

Core comparison lemmas and measurement-agreement translations for the preliminaries chapter.

theorem MIPStarRE.LDT.ConsRel.mono {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] {ψ : QuantumState (ιA × ιB)} {𝒟 : Distribution Question} {A : IdxSubMeas Question Outcome ιA} {B : IdxSubMeas Question Outcome ιB} {δ δ' : Error} (hδ : δ ≤ δ') : ConsRel ψ 𝒟 A B δ → ConsRel ψ 𝒟 A B δ'

Monotonicity of ConsRel in the allowed error parameter.

theorem MIPStarRE.LDT.Preliminaries.postprocessPreservesMeasurements {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (A : SubMeas α ι) (f : α → β) : (postprocess A f).total = A.total

prop:post-processing-preserves.

Postprocessing preserves the total operator, so it preserves both the submeasurement and measurement conditions.

theorem MIPStarRE.LDT.Preliminaries.simeqForMeasurements {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxMeas Question Outcome ι) (δ : Error) : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ ↔ ConsAgreement ψ 𝒟 A B δ

prop:simeq-for-measurements.

theorem MIPStarRE.LDT.Preliminaries.simeqToApprox {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxMeas Question Outcome ι) (δ : Error) : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → BipartiteSDDRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas (2 * δ)

prop:simeq-to-approx.

theorem MIPStarRE.LDT.Preliminaries.simeqToApprox_heterogeneous {Question : Type u_1} {Outcome : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxMeas Question Outcome ιA) (B : IdxMeas Question Outcome ιB) (δ : Error) : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → SDDRel ψ 𝒟 A.toIdxSubMeas.placeLeft B.toIdxSubMeas.placeRight (2 * δ)

Heterogeneous form of prop:simeq-to-approx.

The paper's consistency relation is naturally bipartite: Alice's measurement may act on H_A and Bob's on H_B. This theorem is the same calculation as simeqToApprox, but expressed with the general tensor placements IdxSubMeas.placeLeft and IdxSubMeas.placeRight on ιA × ιB.

theorem MIPStarRE.LDT.Preliminaries.ev_leftTensor_mul_rightTensor_nonneg {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) {X : Quantum.Op ιA} {Y : Quantum.Op ιB} (hX : 0 ≤ X) (hY : 0 ≤ Y) : 0 ≤ ev ψ (leftTensor X * rightTensor Y)

theorem MIPStarRE.LDT.Preliminaries.qMatchMass_leftRight_postprocess_ge {α : Type u_1} {β : Type u_2} {ιA : Type u_3} {ιB : Type u_4} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] [Fintype β] (ψ : QuantumState (ιA × ιB)) (A : SubMeas α ιA) (B : SubMeas α ιB) (f : α → β) : qMatchMass ψ (leftPlacedSubMeas (postprocess A f)) (rightPlacedSubMeas (postprocess B f)) ≥ qMatchMass ψ (leftPlacedSubMeas A) (rightPlacedSubMeas B)

theorem MIPStarRE.LDT.Preliminaries.qBipartiteSSCDefect_postprocess_le {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (ψ : QuantumState (ι × ι)) (M : SubMeas α ι) (f : α → β) : qBipartiteSSCDefect ψ (postprocess M f) ≤ qBipartiteSSCDefect ψ M

Postprocessing can only decrease the bipartite strong self-consistency defect: the total mass is preserved while the diagonal overlap term can only increase.

theorem MIPStarRE.LDT.Preliminaries.simeqDataProcessing_heterogeneous {Question : Type u_1} {α : Type u_2} {β : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] [Fintype β] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxMeas Question α ιA) (B : IdxMeas Question α ιB) (δ : Error) (f : α → β) : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → ConsRel ψ 𝒟 (fun (q : Question) => postprocess (A q).toSubMeas f) (fun (q : Question) => postprocess (B q).toSubMeas f) δ

Heterogeneous form of prop:simeq-data-processing.

This is the paper-faithful opposite-side statement: the two families are first placed on opposite tensor factors of a bipartite state, and only then postprocessed. The generic same-side qConsDefect monotonicity statement is false for arbitrary noncommuting submeasurements.

theorem MIPStarRE.LDT.Preliminaries.simeqDataProcessing {Question : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxMeas Question α ι) (δ : Error) (f : α → β) : ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ → ConsRel ψ 𝒟 (fun (q : Question) => postprocess (A q).toSubMeas f) (fun (q : Question) => postprocess (B q).toSubMeas f) δ

prop:simeq-data-processing.

This is the source-labelled same-space statement. The proof is the heterogeneous opposite-side data-processing theorem specialized to equal local spaces.

theorem MIPStarRE.LDT.Preliminaries.consRelDataProcessing_questionDependent {Question : Type u_1} {α : Type u_2} {β : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype α] [Fintype β] (ψ : QuantumState (ιA × ιB)) (𝒟 : Distribution Question) (A : IdxSubMeas Question α ιA) (B : IdxSubMeas Question α ιB) (δ : Error) (f : Question → α → β) : ConsRel ψ 𝒟 A B δ → ConsRel ψ 𝒟 (fun (q : Question) => postprocess (A q) (f q)) (fun (q : Question) => postprocess (B q) (f q)) δ

Question-dependent postprocessing preserves bipartite consistency.

theorem MIPStarRE.LDT.Preliminaries.consRel_uniform_prod_fst {α : Type u_1} {β : Type u_2} {Outcome : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (A : IdxSubMeas α Outcome ιA) (B : IdxSubMeas α Outcome ιB) (δ : Error) (hAB : ConsRel ψ (uniformDistribution α) A B δ) : ConsRel ψ (uniformDistribution (α × β)) (fun (ab : α × β) => A ab.1) (fun (ab : α × β) => B ab.1) δ

If a uniformly sampled consistency statement depends only on the first coordinate of a product question, it lifts to the full product with the same error.

theorem MIPStarRE.LDT.Preliminaries.consRel_uniform_equiv {α : Type u_1} {β : Type u_2} {Outcome : Type u_3} {ιA : Type u_4} {ιB : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (e : α ≃ β) (ψ : QuantumState (ιA × ιB)) (A : IdxSubMeas α Outcome ιA) (B : IdxSubMeas α Outcome ιB) (δ : Error) : ConsRel ψ (uniformDistribution α) A B δ ↔ ConsRel ψ (uniformDistribution β) (fun (b : β) => A (e.symm b)) (fun (b : β) => B (e.symm b)) δ

Reindexing a uniformly sampled consistency statement along an equivalence.

theorem MIPStarRE.LDT.Preliminaries.qSDDOp_symm {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A B : OpFamily Outcome ι) : qSDDOp ψ A B = qSDDOp ψ B A

qSDDOp is symmetric: swapping the two operator families gives the same squared-distance sum.

theorem MIPStarRE.LDT.Preliminaries.conjTranspose_mul_mono {ι : Type u_1} [Fintype ι] {X Y Z : Quantum.Op ι} (hXY : X ≤ Y) : Matrix.conjTranspose Z * X * Z ≤ Matrix.conjTranspose Z * Y * Z

Loewner-order monotonicity of the matrix sandwich Zᴴ * X * Z. If X ≤ Y then Zᴴ * X * Z ≤ Zᴴ * Y * Z.