Section 12 pasting: comparison common helpers

Shared postprocessing, symmetry, distribution and boundedness helpers for the Section 12 comparison lemmas: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/Common.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The postprocessing lemmas read no state and hold over any ordered ⋆-ring, as hRestrictionToVerticalLine of Co/Pasting/Sandwich/PastedFamilies.lean does, so they serve 𝔓 and K →L[ℂ] K alike. The bipartite lemmas take the symmetric model S : SymModel 𝔓 K as their first explicit argument, in place of the vendored ψ : QuantumState (ι × ι), and keep this file's namespace so that their vendored names pair. The vendored normalization hypothesis hnorm : ψ.IsNormalized of the four _le_one lemmas is dropped (section "Swap symmetry is a theorem": S.ev_one_of_isNormalized takes no hypothesis), so callers pass S and the submeasurements only. Their proofs are the keystone's S.qBipartiteMatchMass_nonneg, S.qBipartiteConsDefect_le_one_of_isNormalized and S.bipartiteConsError_uniform_le_one of Co/Test/Defs.lean.

Not ported

• sqrt_min_le_rpow32: classical, imported.
• hAConsistency_sqrt_bound_of_pos: classical, imported.
• hAConsistency_error_le_nu_of_pos: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/ld-pasting.tex

theorem MIPRE.LIDT.Co.Pasting.postprocess_postprocess {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [Fintype γ] (A : SubMeas α R) (f : α → β) (g : β → γ) : postprocess (postprocess A f) g = postprocess A (g ∘ f)

Postprocessing by f and then by g is postprocessing by g ∘ f.

theorem MIPRE.LIDT.Co.Pasting.postprocess_hRestrictionToVerticalLine_eq_evaluateAt {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (H : SubMeas (MIPStarRE.LDT.Polynomial params.next) R) (u : MIPStarRE.LDT.Point params.next) : (postprocess (hRestrictionToVerticalLine params H (MIPStarRE.LDT.truncatePoint params u)) fun (f : MIPStarRE.LDT.AxisLinePolynomial params.next) => f.toFun (MIPStarRE.LDT.pointHeight params u)) = evaluateAt params.next u H

Reading the restriction of H to the vertical line through truncatePoint u at the height of u is evaluating H at u.

theorem MIPRE.LIDT.Co.Pasting.consRel_uniform_fst {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} {Outcome : Type u_5} [Fintype α] [DecidableEq α] [Nonempty α] [Fintype β] [DecidableEq β] [Nonempty β] [Fintype Outcome] (S : SymModel 𝔓 K) (A B : IdxSubMeas α Outcome 𝔓) (δ : ℝ) : S.ConsRel (MIPStarRE.LDT.uniformDistribution α) A B δ → S.ConsRel (MIPStarRE.LDT.uniformDistribution (α × β)) (fun (ab : α × β) => A ab.1) (fun (ab : α × β) => B ab.1) δ

A consistency relation over uniform questions a persists when an unused uniform coordinate b is adjoined to the question.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteMatchMass_nonneg {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) : 0 ≤ S.qBipartiteMatchMass A B

The bipartite matching mass is nonnegative.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteConsDefect_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : SubMeas Outcome 𝔓) : S.qBipartiteConsDefect A B ≤ 1

A bipartite consistency defect is at most 1.

theorem MIPRE.LIDT.Co.Pasting.bipartiteConsError_uniform_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (S : SymModel 𝔓 K) (A B : IdxSubMeas Question Outcome 𝔓) : S.bipartiteConsError (MIPStarRE.LDT.uniformDistribution Question) A B ≤ 1

Under the uniform question distribution, the averaged bipartite consistency error is at most 1.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteSSCDefect_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : SubMeas Outcome 𝔓) : S.qBipartiteSSCDefect A ≤ 1

A bipartite strong self-consistency defect is at most 1.

theorem MIPRE.LIDT.Co.Pasting.bipartiteSSCError_uniform_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Question] [DecidableEq Question] [Nonempty Question] [Fintype Outcome] (S : SymModel 𝔓 K) (A : IdxSubMeas Question Outcome 𝔓) : S.bipartiteSSCError (MIPStarRE.LDT.uniformDistribution Question) A ≤ 1

Under the uniform question distribution, the averaged bipartite strong self-consistency error is at most 1.