Line interpolation: bad-line event

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

The vendored file mixes two classical declarations, the interpolated vertical line of a tuple of slice answers and the extraction of a mismatching slice when that line differs from a given line polynomial, with two commutation lemmas: evaluating at a point, or restricting to the vertical line through a point, commutes with averaging an indexed submeasurement family over a distribution. The classical pair is imported from the vendored file. The two commutation lemmas read no state, so they are ported generic over an ordered ⋆-ring R, as evaluateAt, hRestrictionToVerticalLine and averageIdxSubMeas are; they serve the local algebra 𝔓 (the vendored Op ι, where all their vendored callers apply them) and K →L[ℂ] K alike.

Not ported

• tupleInterpolatedVerticalLine: classical, imported.
• tupleInterpolatedVerticalLine_ne_gives_exists_some_eval_mismatch: 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.evaluateAt_averageIdxSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Module ℝ R] [PosSMulMono ℝ R] [SMulPosMono ℝ R] [ZeroLEOneClass R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {Question : Type u_2} (u : MIPStarRE.LDT.Point params) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question (MIPStarRE.LDT.Polynomial params) R) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : evaluateAt params u (averageIdxSubMeas 𝒟 A h𝒟) = averageIdxSubMeas 𝒟 (fun (q : Question) => evaluateAt params u (A q)) h𝒟

Evaluating at a point commutes with averaging an indexed polynomial-valued submeasurement family over a sub-probability distribution.

theorem MIPRE.LIDT.Co.Pasting.hRestrictionToVerticalLine_averageIdxSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] [Module ℝ R] [PosSMulMono ℝ R] [SMulPosMono ℝ R] [ZeroLEOneClass R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] {Question : Type u_2} (u : MIPStarRE.LDT.Point params) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question (MIPStarRE.LDT.Polynomial params.next) R) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : hRestrictionToVerticalLine params (averageIdxSubMeas 𝒟 A h𝒟) u = averageIdxSubMeas 𝒟 (fun (q : Question) => hRestrictionToVerticalLine params (A q) u) h𝒟

Restricting to the vertical line through a point commutes with averaging an indexed polynomial-valued submeasurement family over a sub-probability distribution.