Documentation

CompPoly.Bivariate.GuruswamiSudan.Interpolation.LeeOSullivan.Correctness.Basis

Lee-O'Sullivan Basis Correctness Helpers #

Multiplicity, triangularity, and algebraic closure facts for Lee-O'Sullivan basis polynomials.

source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.foldl_range_add_eq_sum {α : Type u_2} [AddCommMonoid α] (f : ℕ → α) (n : ℕ) :
List.foldl (fun (acc : α) (i : ℕ) => acc + f i) 0 (List.range n) = ∑ i ∈ Finset.range n, f i
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.cpoly_natDegree_mul_le_semiring {R : Type u_2} [Semiring R] [BEq R] [LawfulBEq R] (P Q : CPolynomial R) :
(P * Q).natDegree ≤ P.natDegree + Q.natDegree
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.cpoly_natDegree_pow_le {R : Type u_2} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (P : CPolynomial R) {d : ℕ} (hP : P.natDegree ≤ d) (n : ℕ) :
(P ^ n).natDegree ≤ n * d
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_Y_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {P : CBivariate F} {x y : F} {m : ℕ} (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.Y * P).HasMultiplicityAtLeast x y m
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_ofYConstant_mul_eval_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (A : CPolynomial F) {P : CBivariate F} {x y : F} {m : ℕ} (hEval : CPolynomial.eval x A = 0) (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.ofYConstant A * P).HasMultiplicityAtLeast x y (m + 1)
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_linearYDivisor_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R : CPolynomial F) {P : CBivariate F} {x y : F} {m : ℕ} (hEval : CPolynomial.eval x R = y) (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.linearYDivisor R * P).HasMultiplicityAtLeast x y (m + 1)
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_one_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (x y : F) :
CBivariate.HasMultiplicityAtLeast 1 x y 0
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_Y_pow_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (n : ℕ) {P : CBivariate F} {x y : F} {m : ℕ} (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.Y ^ n * P).HasMultiplicityAtLeast x y m
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_ofYConstant_pow_mul_eval_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (A : CPolynomial F) (n : ℕ) {P : CBivariate F} {x y : F} {m : ℕ} (hEval : CPolynomial.eval x A = 0) (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.ofYConstant A ^ n * P).HasMultiplicityAtLeast x y (m + n)
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_linearYDivisor_pow_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R : CPolynomial F) (n : ℕ) {P : CBivariate F} {x y : F} {m : ℕ} (hEval : CPolynomial.eval x R = y) (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.linearYDivisor R ^ n * P).HasMultiplicityAtLeast x y (m + n)
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomial_hasMultiplicityAtLeast {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (idx : ℕ) {x y : F} (hR : CPolynomial.eval x R = y) (hG : CPolynomial.eval x G = 0) :
(leeOSullivanBasisPolynomial R G params idx).HasMultiplicityAtLeast x y params.multiplicity
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomial_satisfiesMultiplicityConstraints {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (idx : ℕ) {points : Array (F × F)} (hR : ∀ point ∈ points.toList, CPolynomial.eval point.1 R = point.2) (hG : ∀ point ∈ points.toList, CPolynomial.eval point.1 G = 0) :
(leeOSullivanBasisPolynomial R G params idx).SatisfiesMultiplicityConstraints points params.multiplicity
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomials_satisfiesMultiplicityConstraints {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {points : Array (F × F)} (hR : ∀ point ∈ points.toList, CPolynomial.eval point.1 R = point.2) (hG : ∀ point ∈ points.toList, CPolynomial.eval point.1 G = 0) (idx : ℕ) :
idx < (leeOSullivanBasisPolynomials R G params).size → ((leeOSullivanBasisPolynomials R G params).getD idx 0).SatisfiesMultiplicityConstraints points params.multiplicity
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofYConstant_one {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] :
CBivariate.ofYConstant 1 = 1
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofYConstant_pow {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (P : CPolynomial F) (n : ℕ) :
CBivariate.ofYConstant (P ^ n) = CBivariate.ofYConstant P ^ n
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.coeff_ofYConstant_mul_outer {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (A : CPolynomial F) (P : CBivariate F) (j : ℕ) :
CPolynomial.coeff (CBivariate.ofYConstant A * P) j = A * CPolynomial.coeff P j
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomial_coeffY_self {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) (idx : ℕ) :
CPolynomial.coeff (leeOSullivanBasisPolynomial R G params idx) idx = G ^ (params.multiplicity - leeOSullivanT params idx)
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomial_coeffY_eq_zero_of_idx_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {idx j : ℕ} (hj : idx < j) :
CPolynomial.coeff (leeOSullivanBasisPolynomial R G params idx) j = 0

Lee basis polynomials have no Y terms above their row index.

source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofYConstant_neg {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (P : CPolynomial F) :
CBivariate.ofYConstant (-P) = -CBivariate.ofYConstant P
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.ofYConstant_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (P Q : CPolynomial F) :
CBivariate.ofYConstant (P - Q) = CBivariate.ofYConstant P - CBivariate.ofYConstant Q
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_ofYConstant_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (A : CPolynomial F) {P : CBivariate F} {x y : F} {m : ℕ} (hP : P.HasMultiplicityAtLeast x y m) :
(CBivariate.ofYConstant A * P).HasMultiplicityAtLeast x y m

Multiplication by a Y-constant polynomial preserves multiplicity constraints already satisfied by the bivariate factor.

source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.hasMultiplicityAtLeast_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {P Q : CBivariate F} {x y : F} {m : ℕ} (hP : P.HasMultiplicityAtLeast x y m) (hQ : Q.HasMultiplicityAtLeast x y m) :
(P - Q).HasMultiplicityAtLeast x y m
source
theorem CompPoly.GuruswamiSudan.LeeOSullivan.satisfiesMultiplicityConstraints_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {P Q : CBivariate F} {points : Array (F × F)} {m : ℕ} (hP : P.SatisfiesMultiplicityConstraints points m) (hQ : Q.SatisfiesMultiplicityConstraints points m) :
(P - Q).SatisfiesMultiplicityConstraints points m