Generic Basis Combination Helpers

Generic finite-Y and basis-combination lemmas used by Lee-O'Sullivan correctness.

theorem CompPoly.cpoly_natDegree_mul_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (P Q : CPolynomial F) : (P * Q).natDegree ≤ P.natDegree + Q.natDegree

theorem CompPoly.cpoly_eval_add {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (x : F) (P Q : CPolynomial F) : CPolynomial.eval x (P + Q) = CPolynomial.eval x P + CPolynomial.eval x Q

theorem CompPoly.cpoly_eval_X {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (x : F) : CPolynomial.eval x CPolynomial.X = x

theorem CompPoly.cpoly_eq_of_toPoly_eq {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] {P Q : CPolynomial F} (h : P.toPoly = Q.toPoly) : P = Q

theorem CompPoly.cpoly_coeff_eq_zero_of_natDegree_lt {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] {P : CPolynomial F} {i : ℕ} (h : P.natDegree < i) : P.coeff i = 0

theorem CompPoly.CBivariate.coeff_neg {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] (P : CBivariate R) (i j : ℕ) : (-P).coeff i j = -P.coeff i j

theorem CompPoly.CBivariate.coeff_sub {R : Type u_1} [Ring R] [BEq R] [LawfulBEq R] [Nontrivial R] (P Q : CBivariate R) (i j : ℕ) : (P - Q).coeff i j = P.coeff i j - Q.coeff i j

theorem CompPoly.CBivariate.coeff_CC_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (c : R) (Q : CBivariate R) (i j : ℕ) : (CC c * Q).coeff i j = c * Q.coeff i j

theorem CompPoly.CBivariate.coeff_X_mul_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (j : ℕ) : (X * Q).coeff 0 j = 0

theorem CompPoly.CBivariate.coeff_X_mul_succ {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (Q : CBivariate R) (i j : ℕ) : (X * Q).coeff (i + 1) j = Q.coeff i j

theorem CompPoly.CBivariate.evalEval_CC_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c x y : F) (Q : CBivariate F) : evalEval x y (CC c * Q) = c * evalEval x y Q

theorem CompPoly.CBivariate.evalEval_X_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (x y : F) (Q : CBivariate F) : evalEval x y (X * Q) = x * evalEval x y Q

theorem CompPoly.CBivariate.evalEval_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (x y : F) (P Q : CBivariate F) : evalEval x y (P - Q) = evalEval x y P - evalEval x y Q

theorem CompPoly.CBivariate.hasseDerivative_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a b : ℕ) (P Q : CBivariate F) : hasseDerivative a b (P - Q) = hasseDerivative a b P - hasseDerivative a b Q

theorem CompPoly.CBivariate.hasseDerivative_CC_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (a b : ℕ) (Q : CBivariate F) : hasseDerivative a b (CC c * Q) = CC c * hasseDerivative a b Q

theorem CompPoly.CBivariate.hasseDerivative_X_mul_zero_xOrder {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (b : ℕ) (Q : CBivariate F) : hasseDerivative 0 b (X * Q) = X * hasseDerivative 0 b Q

theorem CompPoly.CBivariate.hasseDerivative_X_mul_succ_xOrder {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a b : ℕ) (Q : CBivariate F) : hasseDerivative (a + 1) b (X * Q) = X * hasseDerivative (a + 1) b Q + hasseDerivative a b Q

theorem CompPoly.CBivariate.hasseDerivativeEval_CC_mul {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (c : F) (a b : ℕ) (x y : F) (Q : CBivariate F) : hasseDerivativeEval a b x y (CC c * Q) = c * hasseDerivativeEval a b x y Q

theorem CompPoly.CBivariate.hasseDerivativeEval_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a b : ℕ) (x y : F) (P Q : CBivariate F) : hasseDerivativeEval a b x y (P - Q) = hasseDerivativeEval a b x y P - hasseDerivativeEval a b x y Q

theorem CompPoly.CBivariate.hasseDerivativeEval_X_mul_zero_xOrder {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (b : ℕ) (x y : F) (Q : CBivariate F) : hasseDerivativeEval 0 b x y (X * Q) = x * hasseDerivativeEval 0 b x y Q

theorem CompPoly.CBivariate.hasseDerivativeEval_X_mul_succ_xOrder {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a b : ℕ) (x y : F) (Q : CBivariate F) : hasseDerivativeEval (a + 1) b x y (X * Q) = x * hasseDerivativeEval (a + 1) b x y Q + hasseDerivativeEval a b x y Q

def CompPoly.GuruswamiSudan.koetterYCap (params : GSInterpParams) : ℕ

Finite Y cap shared by positive-Y-weight interpolation proofs.

theorem CompPoly.GuruswamiSudan.coeff_ofYCoefficient {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] [DecidableEq F] (j : ℕ) (P : CPolynomial F) (i k : ℕ) : (CBivariate.ofYCoefficient j P).coeff i k = if k = j then P.coeff i else 0

theorem CompPoly.GuruswamiSudan.coeff_ofYConstant {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (P : CPolynomial F) (i j : ℕ) : (CBivariate.ofYConstant P).coeff i j = if j = 0 then P.coeff i else 0

theorem CompPoly.GuruswamiSudan.coeff_ofYConstant_mul {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (A : CPolynomial F) (P : CBivariate F) (i j : ℕ) : (CBivariate.ofYConstant A * P).coeff i j = (A * (↑P).coeff j).coeff i

theorem CompPoly.GuruswamiSudan.natWeightedDegree_ofYConstant_mul_le {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (A : CPolynomial F) (P : CBivariate F) (w : ℕ) : (CBivariate.ofYConstant A * P).natWeightedDegree 1 w ≤ A.natDegree + P.natWeightedDegree 1 w

theorem CompPoly.GuruswamiSudan.validWitness_coeffY_eq_zero_of_yCap_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {params : GSInterpParams} {Q : CBivariate F} (hMessage : ¬params.messageDegree ≤ 1) (hQ : ValidInterpolationWitness points params Q) {j : ℕ} (hj : koetterYCap params < j) : (↑Q).coeff j = 0

theorem CompPoly.GuruswamiSudan.ofYConstant_zero {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] : CBivariate.ofYConstant 0 = 0

theorem CompPoly.GuruswamiSudan.ofYConstant_add {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (P Q : CPolynomial F) : CBivariate.ofYConstant (P + Q) = CBivariate.ofYConstant P + CBivariate.ofYConstant Q

theorem CompPoly.GuruswamiSudan.ofYConstant_C {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (c : F) : CBivariate.ofYConstant (CPolynomial.C c) = CBivariate.CC c

theorem CompPoly.GuruswamiSudan.ofYConstant_mul {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (P Q : CPolynomial F) : CBivariate.ofYConstant (P * Q) = CBivariate.ofYConstant P * CBivariate.ofYConstant Q

theorem CompPoly.GuruswamiSudan.ofYConstant_X_mul {F : Type u_1} [Semiring F] [BEq F] [LawfulBEq F] [Nontrivial F] (P : CPolynomial F) : CBivariate.ofYConstant (CPolynomial.X * P) = CBivariate.X * CBivariate.ofYConstant P

theorem CompPoly.GuruswamiSudan.cpoly_eq_zero_of_val_size_eq_zero {F : Type u_1} [Zero F] [BEq F] [LawfulBEq F] (P : CPolynomial F) (hsize : Array.size ↑P = 0) : P = 0

theorem CompPoly.GuruswamiSudan.hasseDerivativeEval_ofYConstant_mul_eq_eval_mul_of_lower {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (x y : F) (b : ℕ) (A : CPolynomial F) (P : CBivariate F) (order : ℕ) : (∀ a < order, CBivariate.hasseDerivativeEval a b x y P = 0) → CBivariate.hasseDerivativeEval order b x y (CBivariate.ofYConstant A * P) = CPolynomial.eval x A * CBivariate.hasseDerivativeEval order b x y P

theorem CompPoly.GuruswamiSudan.hasseDerivativeEval_ofYConstant_mul_eq_zero_of_lower {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (x y : F) (b : ℕ) (A : CPolynomial F) (P : CBivariate F) (order : ℕ) (hLower : ∀ a ≤ order, CBivariate.hasseDerivativeEval a b x y P = 0) : CBivariate.hasseDerivativeEval order b x y (CBivariate.ofYConstant A * P) = 0

theorem CompPoly.GuruswamiSudan.foldl_add_congr_terms {α : Type u_1} [Add α] (xs : List ℕ) (f g : ℕ → α) (z : α) (h : ∀ x ∈ xs, f x = g x) : List.foldl (fun (out : α) (x : ℕ) => out + f x) z xs = List.foldl (fun (out : α) (x : ℕ) => out + g x) z xs

theorem CompPoly.GuruswamiSudan.foldl_add_distrib_terms_aux {α : Type u_1} [AddCommMonoid α] (xs : List ℕ) (f g : ℕ → α) (a b : α) : List.foldl (fun (out : α) (x : ℕ) => out + (f x + g x)) (a + b) xs = List.foldl (fun (out : α) (x : ℕ) => out + f x) a xs + List.foldl (fun (out : α) (x : ℕ) => out + g x) b xs

theorem CompPoly.GuruswamiSudan.foldl_add_distrib_terms {α : Type u_1} [AddCommMonoid α] (xs : List ℕ) (f g : ℕ → α) : List.foldl (fun (out : α) (x : ℕ) => out + (f x + g x)) 0 xs = List.foldl (fun (out : α) (x : ℕ) => out + f x) 0 xs + List.foldl (fun (out : α) (x : ℕ) => out + g x) 0 xs

theorem CompPoly.GuruswamiSudan.foldl_add_single_beq_of_not_mem {α : Type u_1} [AddCommMonoid α] (xs : List ℕ) (target : ℕ) (term acc : α) (hnot : target ∉ xs) : List.foldl (fun (out : α) (idx : ℕ) => out + if (idx == target) = true then term else 0) acc xs = acc

theorem CompPoly.GuruswamiSudan.foldl_add_single_beq_of_nodup_mem {α : Type u_1} [AddCommMonoid α] (xs : List ℕ) (target : ℕ) (term : α) (hnodup : xs.Nodup) (hmem : target ∈ xs) : List.foldl (fun (out : α) (idx : ℕ) => out + if (idx == target) = true then term else 0) 0 xs = term

def CompPoly.GuruswamiSudan.koetterBasisCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) : CBivariate F

def CompPoly.GuruswamiSudan.koetterBasisSpanContains {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (basis : Array (CBivariate F)) (Q : CBivariate F) : Prop

theorem CompPoly.GuruswamiSudan.koetterBasisCombination_eq_zero_of_weights_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) (hzero : ∀ idx < basis.size, weights idx = 0) : koetterBasisCombination weights basis = 0

theorem CompPoly.GuruswamiSudan.coeff_koetterBasisCombination {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (weights : ℕ → CPolynomial F) (basis : Array (CBivariate F)) (i j : ℕ) : (koetterBasisCombination weights basis).coeff i j = List.foldl (fun (out : F) (idx : ℕ) => out + (CBivariate.ofYConstant (weights idx) * basis.getD idx 0).coeff i j) 0 (List.range basis.size)