Preliminary comparison theorems: bipartite self-consistency (completion)

Completion-transfer lemmas for bipartite self-consistency. The constant Unit-family reductions identify sddError and sscError with their pointwise forms, and the later lemmas compare a submeasurement with its completion.

References

• references/ldt-paper/preliminaries.tex
• blueprint/src/chapter/ch03_preliminaries.tex

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

For a constant Unit-indexed family, sddError reduces to qSDD.

theorem MIPStarRE.LDT.Preliminaries.constFamily_ssc_unit {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : SubMeas Outcome ι) : sscError ψ (uniformDistribution Unit) (constSubMeasFamily A) = qSSCDefect ψ A

For a constant Unit-indexed family, sscError reduces to qSSCDefect.

theorem MIPStarRE.LDT.Preliminaries.completion_self_distance {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (B : SubMeas Outcome ι) (a0 : Outcome) : qSDD ψ B (completeAtOutcome B a0).toSubMeas = ev ψ ((1 - B.total) * (1 - B.total))

Completing B at a0 changes only the missing mass, so the self-distance is exactly the squared residual mass.

theorem MIPStarRE.LDT.Preliminaries.evaluateAt_completeAtOutcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (H : SubMeas (Polynomial params) ι) (h0 : Polynomial params) (u : Point params) : evaluateAt params u (completeAtOutcome H h0).toSubMeas = (completeAtOutcome (evaluateAt params u H) (h0.toFun u)).toSubMeas

Evaluating a completed polynomial submeasurement at a point is the same as completing the evaluated submeasurement at the induced outcome.

theorem MIPStarRE.LDT.Preliminaries.qBipartiteConsDefect_completeAtOutcome_right_le {Outcome : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] [Fintype Outcome] (ψ : QuantumState (ιA × ιB)) (A : Measurement Outcome ιA) (B : SubMeas Outcome ιB) (a0 : Outcome) : qBipartiteConsDefect ψ A.toSubMeas (completeAtOutcome B a0).toSubMeas ≤ qBipartiteConsDefect ψ A.toSubMeas B + ev ψ (rightTensor (1 - B.total))

Completing the right submeasurement can increase the bipartite consistency defect by at most the residual completion mass 1 - B.total.