Line interpolation: bad-line event

Definitions and lemmas for tupleInterpolatedVerticalLine and mismatch extraction in the line-interpolation argument.

References

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

noncomputable def MIPStarRE.LDT.Pasting.tupleInterpolatedVerticalLine (params : Parameters) [FieldModel params.q] {k : ℕ} (u : Point params) (xs : PointTuple params k) (gs : GHatTupleOutcome params k) : AxisLinePolynomial params.next

Equations

• One or more equations did not get rendered due to their size.

theorem MIPStarRE.LDT.Pasting.evaluateAt_averageIdxSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {Question : Type u_2} (u : Point params) (𝒟 : Distribution Question) (A : IdxSubMeas Question (Polynomial params) ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : evaluateAt params u (averageIdxSubMeas 𝒟 A h𝒟) = averageIdxSubMeas 𝒟 (fun (q : Question) => evaluateAt params u (A q)) h𝒟

theorem MIPStarRE.LDT.Pasting.hRestrictionToVerticalLine_averageIdxSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] {Question : Type u_2} (u : Point params) (𝒟 : Distribution Question) (A : IdxSubMeas Question (Polynomial params.next) ι) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : hRestrictionToVerticalLine params (averageIdxSubMeas 𝒟 A h𝒟) u = averageIdxSubMeas 𝒟 (fun (q : Question) => hRestrictionToVerticalLine params (A q) u) h𝒟

theorem MIPStarRE.LDT.Pasting.tupleInterpolatedVerticalLine_ne_gives_exists_some_eval_mismatch (params : Parameters) [FieldModel params.q] {k : ℕ} (u : Point params) (xs : PointTuple params k) (hxs : Function.Injective xs) (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) (_hGlobal : IsGloballyConsistent params xs gs) (f : AxisLinePolynomial params.next) (hne : tupleInterpolatedVerticalLine params u xs gs ≠ f) : ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), (Option.get (gs i) hiSome).toFun u ≠ f.toFun (xs i)