Triangle Inequalities for State-Dependent Distance: Core

This module contains the main triangle-substitution estimates for approximate measurements.

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

Symmetry of the question-level state-dependent distance.

theorem MIPStarRE.LDT.Preliminaries.sddRel_symm {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A B : IdxSubMeas Question Outcome ι) (δ : Error) : SDDRel ψ 𝒟 A B δ → SDDRel ψ 𝒟 B A δ

Symmetry of the state-dependent distance relation.

theorem MIPStarRE.LDT.Preliminaries.triangleInequalityForVectorsSquared {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (D : κ → Quantum.Op ι) : ev ψ ((∑ i : κ, D i).conjTranspose * ∑ i : κ, D i) ≤ ↑(Fintype.card κ) * ∑ i : κ, ev ψ (Matrix.conjTranspose (D i) * D i)

prop:triangle-inequality-for-vectors-squared.

For a finite family of operators Dᵢ, the squared norm of the summed vector (∑ᵢ Dᵢ) ψ is controlled by the cardinality times the sum of the squared norms of the individual vectors Dᵢ ψ.

theorem MIPStarRE.LDT.Preliminaries.subMeas_total_ev_gap_abs_le_sqrt_card_qSDD {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (A B : SubMeas Outcome ι) : |ev ψ A.total - ev ψ B.total| ≤ √↑(Fintype.card Outcome) * √(qSDD ψ A B)

The expectation of the difference of two submeasurement totals is controlled by the state-dependent distance between the two outcome families, with the finite-outcome Cauchy--Schwarz loss.

This is the total-operator analogue of the matching-mass estimates used in triangleSub. It is useful precisely when the right-register families are submeasurements rather than measurements, so that their total operators need not be the identity.

Elementary max bound

theorem MIPStarRE.LDT.Preliminaries.max_zero_add_le (x y : Error) : max 0 (x + y) ≤ max 0 x + |y|

Adding y inside max 0 changes the value by at most |y|.

theorem MIPStarRE.LDT.Preliminaries.triangleSub {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxMeas Question Outcome ι) (C : IdxSubMeas Question Outcome ι) (δ ε : Error) (hAC : ConsRel ψ 𝒟 A.toIdxSubMeas C δ) (hAB : SDDRel ψ 𝒟 A.toIdxSubMeas.liftLeft B.toIdxSubMeas.liftLeft ε) : ConsRel ψ 𝒟 B.toIdxSubMeas C (δ + √ε)

prop:triangle-sub.

The proof rewrites both consistency errors as ev ψ (I ⊗ C.total) - Σₐ ev ψ (...), bound the overlap difference by Cauchy-Schwarz using ev_abs_mul_le_sqrt and subMeas_diagMass_le_one, then average with avgOver_abs_le_sqrt_of_pointwise.

This signature is the downstream API needed by Stream D.

theorem MIPStarRE.LDT.Preliminaries.triangleSub_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) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxMeas Question Outcome ιA) (C : IdxSubMeas Question Outcome ιB) (δ ε : Error) (hAC : ConsRel ψ 𝒟 A.toIdxSubMeas C δ) (hAB : SDDRel ψ 𝒟 A.toIdxSubMeas.placeLeft B.toIdxSubMeas.placeLeft ε) : ConsRel ψ 𝒟 B.toIdxSubMeas C (δ + √ε)

Heterogeneous left-register substitution.

This is the same proof as triangleSub, with the two left families placed on H_A and the right family placed on H_B. It is the form needed when the paper's final triangle replaces Alice's polynomial measurement while Bob's point measurement is held fixed.

Right-register variant of triangleSub

theorem MIPStarRE.LDT.Preliminaries.triangleSub_right {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question Outcome ι) (B D : IdxMeas Question Outcome ι) (δ ε : Error) (hAB : ConsRel ψ 𝒟 A B.toIdxSubMeas δ) (hBD : SDDRel ψ 𝒟 B.toIdxSubMeas.liftRight D.toIdxSubMeas.liftRight ε) : ConsRel ψ 𝒟 A D.toIdxSubMeas (δ + √ε)

theorem MIPStarRE.LDT.Preliminaries.triangleSub_right_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) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question Outcome ιA) (B D : IdxMeas Question Outcome ιB) (δ ε : Error) (hAB : ConsRel ψ 𝒟 A B.toIdxSubMeas δ) (hBD : SDDRel ψ 𝒟 B.toIdxSubMeas.placeRight D.toIdxSubMeas.placeRight ε) : ConsRel ψ 𝒟 A D.toIdxSubMeas (δ + √ε)

Heterogeneous right-register substitution.

This is the same proof as triangleSub_right, with the left family placed on H_A and the two right families placed on H_B. It is the form needed for the paper-facing two-prover strategy in thm:main-formal, where Alice's and Bob's local Hilbert spaces are not assumed to be the same.

theorem MIPStarRE.LDT.Preliminaries.triangleSub_right_subMeas_totalGap {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B D : IdxSubMeas Question Outcome ι) (δ ε η : Error) (hAB : ConsRel ψ 𝒟 A B δ) (hBD : SDDRel ψ 𝒟 B.liftRight D.liftRight ε) (hTotal : (avgOver 𝒟 fun (q : Question) => |ev ψ (leftTensor (A q).total * rightTensor (D q).total) - ev ψ (leftTensor (A q).total * rightTensor (B q).total)|) ≤ η) : ConsRel ψ 𝒟 A D (δ + √ε + η)

Right-register substitution for submeasurements, with the total-overlap displacement stated explicitly.

For complete right-register measurements the total-overlap term ev ψ (A_total ⊗ B_total) is independent of the right family. For general submeasurements this term may change. The lemma therefore separates the usual state-dependent-distance contribution from the averaged displacement of the right total operator.

theorem MIPStarRE.LDT.Preliminaries.triangleSub_right_subMeas_total_le {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B D : IdxSubMeas Question Outcome ι) (δ ε : Error) (hAB : ConsRel ψ 𝒟 A B δ) (hBD : SDDRel ψ 𝒟 B.liftRight D.liftRight ε) (hTotalLe : ∀ (q : Question), ev ψ (leftTensor (A q).total * rightTensor (D q).total) ≤ ev ψ (leftTensor (A q).total * rightTensor (B q).total)) : ConsRel ψ 𝒟 A D (δ + √ε)

Right-register substitution for submeasurements when the right total overlap is monotone in the replacement direction.

The general submeasurement form triangleSub_right_subMeas_totalGap includes the absolute displacement of the total-overlap term. In the special case where the new right family has no larger total overlap with the fixed left family, this displacement is not needed: increasing the total is the only way in which the total term can worsen the consistency defect. The remaining contribution is exactly the usual matching-mass Cauchy--Schwarz term.