Lee-O'Sullivan Interpolation Completeness #
Completeness theorems and public context wrapper for Lee-O'Sullivan interpolation.
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanPositiveInterpolate_complete_of_row
{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}
(hdistinct : DistinctXCoordinates points)
(hHigh : ¬params.messageDegree ≤ 1)
{row : PolynomialRow F}
{rowDegree : ℕ}
(hrowSpan :
row ∈ (leeOSullivanBasisRowsWithRG
(CPolynomial.interpolateCoefficientFormWithVanishing E
(V.vanishingPolynomial (Array.map (fun (point : F × F) => point.1) points)) points)
(V.vanishingPolynomial (Array.map (fun (point : F × F) => point.1) points)) params).RowSpan)
(hrowDegree : PolynomialMatrix.rowShiftedDegree? row (leeOSullivanShifts params) = some rowDegree)
(hrowBound : rowDegree ≤ params.weightedDegreeBound)
:
∃ (Q : CBivariate F), leeOSullivanPositiveInterpolate V E reducer points params = some Q
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanPositiveInterpolate_complete_of_span
{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}
(hdistinct : DistinctXCoordinates points)
(hHigh : ¬params.messageDegree ≤ 1)
(hQ : ValidInterpolationWitness points params Q)
(hspan :
koetterBasisSpanContains
(leeOSullivanBasisPolynomials
(CPolynomial.interpolateCoefficientFormWithVanishing E
(V.vanishingPolynomial (Array.map (fun (point : F × F) => point.1) points)) points)
(V.vanishingPolynomial (Array.map (fun (point : F × F) => point.1) points)) params)
Q)
:
∃ (Q : CBivariate F), leeOSullivanPositiveInterpolate V E reducer points params = some Q
theorem
CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanInterpolate_complete
{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}
(hdistinct : DistinctXCoordinates points)
(hExists : ∃ (Q : CBivariate F), ValidInterpolationWitness points params Q)
:
∃ (Q : CBivariate F), leeOSullivanInterpolate V E reducer points params = some Q
Distinct-input completeness for the executable Lee-O'Sullivan interpolation operation.
def
CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanInterpContext
{F : Type u_1}
[Field F]
[BEq F]
[LawfulBEq F]
[DecidableEq F]
(V : CPolynomial.VanishingPolynomialContext F)
(E : CPolynomial.BatchEvalContext F)
(reducer : PolynomialMatrix.ShiftedRowReducerContext F)
:
Public Lee-O'Sullivan interpolation backend context.