Line interpolation: averaging and tensor helpers

The counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/LineInterpolation/Averaging.lean in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").

The vendored file mixes five classical lemmas (the comparison of an average over distinct tuples with the uniform average plus the total-variation distance, and three max 0 estimates, the last of which is Jensen's inequality for max 0 under an average) with three bipartite lemmas: averaging the left family of an indexed submeasurement over a distribution averages the matching mass and the total overlap, and does not increase the consistency defect. The classical lemmas are imported from the vendored file. 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 families are local, in 𝔓 (the vendored Op ι). No statement carries a swap or normalization hypothesis, the vendored statements having none.

Not ported

• avgOver_distinct_bounded_le_avgOver_uniform_add_tv: classical, imported.
• avgOver_distinct_bounded_le_avgOver_uniform_add_tv_of_any_k: classical, imported.
• max_zero_add_le: classical, imported.
• max_zero_mul_add_le: classical, imported.
• max_zero_avgOver_le_avgOver_max_zero: classical, imported.

References

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

• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch09_pasting.tex

theorem MIPRE.LIDT.Co.Pasting.qBipartiteMatchMass_averageIdxSubMeas_left {𝔓 : 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 Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : SubMeas Outcome 𝔓) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : S.qBipartiteMatchMass (averageIdxSubMeas 𝒟 A h𝒟) B = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => S.qBipartiteMatchMass (A q) B

The bipartite matching mass of an averaged left family against B is the average of the matching masses.

theorem MIPRE.LIDT.Co.Pasting.ev_opTensor_total_averageIdxSubMeas_left {𝔓 : 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 Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : SubMeas Outcome 𝔓) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : S.ev (S.opTensor (averageIdxSubMeas 𝒟 A h𝒟).total B.total) = MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => S.ev (S.opTensor (A q).total B.total)

The total overlap of an averaged left family with B is the average of the total overlaps.

theorem MIPRE.LIDT.Co.Pasting.qBipartiteConsDefect_averageIdxSubMeas_left_le {𝔓 : 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 Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (B : SubMeas Outcome 𝔓) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : S.qBipartiteConsDefect (averageIdxSubMeas 𝒟 A h𝒟) B ≤ MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => S.qBipartiteConsDefect (A q) B

Averaging the left family does not increase the bipartite consistency defect: the defect of the average is at most the average of the defects (Jensen for max 0).