Line interpolation: core API

Interpolation-support, vertical-line restriction, and completed-slice interpolation lemmas from ld-pasting.tex that form the foundation for the line-interpolation estimates.

References

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

theorem MIPStarRE.LDT.Pasting.axisLinePolynomial_ne_gives_support_eval_ne (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (hxs : Function.Injective xs) (σ : Finset (Fin k)) (hσcard : σ.card = params.d + 1) {f g : AxisLinePolynomial params.next} (hne : f ≠ g) : ∃ i ∈ σ, f.toFun (xs i) ≠ g.toFun (xs i)

theorem MIPStarRE.LDT.Pasting.nonglobal_gives_slice_mismatch_against_interpolant (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (gs : GHatTupleOutcome params k) (hNGlobal : ¬IsGloballyConsistent params xs gs) : ∃ (i : Fin k) (hiSome : Option.isSome (gs i) = true), Polynomial.restrictAtHeight params (interpolateCompletedSlices params k xs gs) (xs i) ≠ Option.get (gs i) hiSome

noncomputable def MIPStarRE.LDT.Pasting.interpolationSupportSubset {params : Parameters} [FieldModel params.q] {k : ℕ} (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) : Finset (Fin k)

The chosen d+1 interpolation support inside gHatTupleSupport.

Equations

• MIPStarRE.LDT.Pasting.interpolationSupportSubset gs hEligible = (MIPStarRE.LDT.Pasting.interpolationSupportWitness gs hEligible).support

theorem MIPStarRE.LDT.Pasting.interpolationSupportSubset_subset {params : Parameters} [FieldModel params.q] {k : ℕ} (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) : interpolationSupportSubset gs hEligible ⊆ gHatTupleSupport gs

theorem MIPStarRE.LDT.Pasting.interpolationSupportSubset_card {params : Parameters} [FieldModel params.q] {k : ℕ} (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) : (interpolationSupportSubset gs hEligible).card = params.d + 1

theorem MIPStarRE.LDT.Pasting.restrictToAxisParallelLine_apply (params : Parameters) [FieldModel params.q] (h : Polynomial params.next) (ℓ : AxisParallelLine params.next) (t : Fq params.next) : (Polynomial.restrictToAxisParallelLine params.next h ℓ).toFun t = h.toFun (ℓ.pointAt t)

theorem MIPStarRE.LDT.Pasting.restrictToVerticalLine_eval_eq_restrictAtHeight_eval (params : Parameters) [FieldModel params.q] (h : Polynomial params.next) (u : Point params) (x : Fq params) : (Polynomial.restrictToAxisParallelLine params.next h { base := appendPoint params u zeroCoord, direction := lastCoord params }).toFun x = (Polynomial.restrictAtHeight params h x).toFun u

theorem MIPStarRE.LDT.Pasting.interpolateCompletedSlicesFromSupport_restrictAtHeight_poly_eq_get_of_mem (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (hxs : Function.Injective xs) (gs : GHatTupleOutcome params k) (σ : Finset (Fin k)) (hσsubset : σ ⊆ gHatTupleSupport gs) (hσcard : σ.card = params.d + 1) {i : Fin k} (hi : i ∈ σ) : (MvPolynomial.eval₂Hom MvPolynomial.C (Polynomial.restrictAtHeightCoordinateMap params (xs i))) (interpolateCompletedSlicesFromSupport params xs gs σ hσsubset hσcard).poly = (Option.get (gs i) ⋯).poly

theorem MIPStarRE.LDT.Pasting.interpolateCompletedSlices_restrictAtHeight_eq_get_of_mem_supportSubset (params : Parameters) [FieldModel params.q] {k : ℕ} (xs : PointTuple params k) (hxs : Function.Injective xs) (gs : GHatTupleOutcome params k) (hEligible : InterpolationEligible params gs) {i : Fin k} (hi : i ∈ interpolationSupportSubset gs hEligible) : (Polynomial.restrictAtHeight params (interpolateCompletedSlices params k xs gs) (xs i)).poly = (Option.get (gs i) ⋯).poly