Lee-O'Sullivan Interpolation Soundness #
Soundness for the executable Lee-O'Sullivan interpolation operation.
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanInterpolate_sound
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(V : CPolynomial.VanishingPolynomialContext F)
(E : CPolynomial.BatchEvalContext F)
(reducer : PolynomialMatrix.ShiftedRowReducerContext F)
{points : Array (F × F)}
{params : GSInterpParams}
{Q : CBivariate F}
(h : leeOSullivanInterpolate V E reducer points params = some Q)
:
ValidInterpolationWitness points params Q
Soundness for the executable Lee-O'Sullivan interpolation operation.