Roth-Ruckenstein Correctness Support

Coefficient, composition, and root-filter lemmas used by the Roth-Ruckenstein correctness proofs.

theorem CompPoly.GuruswamiSudan.cpoly_val_coeff_ofArray {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (coeffs : Array R) (i : ℕ) : (↑(CPolynomial.ofArray coeffs)).coeff i = coeffs.getD i 0

theorem CompPoly.GuruswamiSudan.cpoly_coeff_eq_zero_of_size_le {R : Type u_1} [Zero R] (p : CPolynomial R) {i : ℕ} (h : Array.size ↑p ≤ i) : p.coeff i = 0

theorem CompPoly.GuruswamiSudan.cpoly_size_eq_natDegree_succ_of_ne_zero {R : Type u_1} [Zero R] {p : CPolynomial R} (hp : p ≠ 0) : Array.size ↑p = p.natDegree + 1

theorem CompPoly.GuruswamiSudan.cpoly_coeff_natDegree_ne_zero_of_ne_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {p : CPolynomial R} (hp : p ≠ 0) : p.coeff p.natDegree ≠ 0

theorem CompPoly.GuruswamiSudan.cpoly_coeff_eq_zero_of_natDegree_lt {R : Type u_1} [Zero R] (p : CPolynomial R) {i : ℕ} (hi : p.natDegree < i) : p.coeff i = 0

theorem CompPoly.GuruswamiSudan.cpoly_coeff_dropXPower {R : Type u_1} [Zero R] (p : CPolynomial R) (n i : ℕ) : (p.dropXPower n).coeff i = p.coeff (i + n)

theorem CompPoly.GuruswamiSudan.cpoly_toPoly_eq_X_pow_mul_dropXPower_of_coeff_eq_zero_lt {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) (hzero : ∀ i < n, p.coeff i = 0) : p.toPoly = Polynomial.X ^ n * (p.dropXPower n).toPoly

theorem CompPoly.GuruswamiSudan.cbivar_coeff_divXPower {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (n i j : ℕ) : (Q.divXPower n).coeff i j = Q.coeff (i + n) j

theorem CompPoly.GuruswamiSudan.cbivar_coeffY_divXPower {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (n j : ℕ) : (↑(Q.divXPower n)).coeff j = ((↑Q).coeff j).dropXPower n

theorem CompPoly.GuruswamiSudan.cbivar_coeff_eq_zero_of_y_size_le {R : Type u_1} [Zero R] (Q : CBivariate R) {i j : ℕ} (hj : Array.size ↑Q ≤ j) : Q.coeff i j = 0

theorem CompPoly.GuruswamiSudan.initialCoefficientPolynomial_coeff_fold {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) (j : ℕ) (ys : List ℕ) (out : CPolynomial F) : ys.Nodup → (List.foldl (fun (out : CPolynomial F) (y : ℕ) => out + CPolynomial.monomial y (Q.coeff 0 y)) out ys).coeff j = out.coeff j + if j ∈ ys then Q.coeff 0 j else 0

theorem CompPoly.GuruswamiSudan.initialCoefficientPolynomial_coeff_of_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (Q : CBivariate F) {j : ℕ} (hj : j < Array.size ↑Q) : (initialCoefficientPolynomial Q).coeff j = Q.coeff 0 j

theorem CompPoly.GuruswamiSudan.cpoly_xAdicOrder?_some_coeff_ne {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} {i : ℕ} (h : p.xAdicOrder? = some i) : p.coeff i ≠ 0

theorem CompPoly.GuruswamiSudan.cpoly_xAdicOrder?_some_coeff_eq_zero_of_lt {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} {order i : ℕ} (h : p.xAdicOrder? = some order) (hi : i < order) : p.coeff i = 0

theorem CompPoly.GuruswamiSudan.cpoly_xAdicOrder?_none_eq_zero {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {p : CPolynomial R} (h : p.xAdicOrder? = none) : p = 0

def CompPoly.GuruswamiSudan.xAdicStep {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) (best : Option ℕ) (y : ℕ) : Option ℕ

def CompPoly.GuruswamiSudan.xAdicWitness {R : Type u_1} [Zero R] (Q : CBivariate R) (best : Option ℕ) : Prop

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_step_witness {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (best : Option ℕ) {y : ℕ} (hw : xAdicWitness Q best) (hy : y < Array.size ↑Q) : xAdicWitness Q (xAdicStep Q best y)

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_fold_witness {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] (Q : CBivariate R) (ys : List ℕ) (best : Option ℕ) : xAdicWitness Q best → (∀ y ∈ ys, y < Array.size ↑Q) → xAdicWitness Q (List.foldl (xAdicStep Q) best ys)

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_some_exists {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {Q : CBivariate R} {order : ℕ} (h : Q.xAdicOrder? = some order) : ∃ y < Array.size ↑Q, Q.coeff order y ≠ 0

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_step_some_le_best {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) {best : Option ℕ} {current result y : ℕ} (hbest : best = some current) (hstep : xAdicStep Q best y = some result) : result ≤ current

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_step_some_le_row {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) {best : Option ℕ} {rowOrder result y : ℕ} (hrow : ((↑Q).coeff y).xAdicOrder? = some rowOrder) (hstep : xAdicStep Q best y = some result) : result ≤ rowOrder

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_fold_some_le_best {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) (ys : List ℕ) (best : Option ℕ) (current result : ℕ) : best = some current → List.foldl (xAdicStep Q) best ys = some result → result ≤ current

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_fold_some_le_row {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) (ys : List ℕ) (best : Option ℕ) (result y rowOrder : ℕ) : List.foldl (xAdicStep Q) best ys = some result → y ∈ ys → ((↑Q).coeff y).xAdicOrder? = some rowOrder → result ≤ rowOrder

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_some_coeff_eq_zero_of_lt {R : Type u_1} [Zero R] [BEq R] [LawfulBEq R] {Q : CBivariate R} {order i y : ℕ} (h : Q.xAdicOrder? = some order) (hi : i < order) : Q.coeff i y = 0

theorem CompPoly.GuruswamiSudan.cbivar_toPoly_eq_C_X_pow_mul_divXPower_of_xAdicOrder {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} {order : ℕ} (horder : Q.xAdicOrder? = some order) : Q.toPoly = Polynomial.C (Polynomial.X ^ order) * (Q.divXPower order).toPoly

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_fold_none {R : Type u_1} [Zero R] [BEq R] (Q : CBivariate R) (ys : List ℕ) (best : Option ℕ) : List.foldl (xAdicStep Q) best ys = none → best = none ∧ ∀ y ∈ ys, ((↑Q).coeff y).xAdicOrder? = none

theorem CompPoly.GuruswamiSudan.cbivar_xAdicOrder?_none_eq_zero {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] {Q : CBivariate F} (h : Q.xAdicOrder? = none) : Q = 0

theorem CompPoly.GuruswamiSudan.cpoly_dropXPower_add {R : Type u_1} [Zero R] (p : CPolynomial R) (m n : ℕ) : (p.dropXPower m).dropXPower n = p.dropXPower (m + n)

theorem CompPoly.GuruswamiSudan.dropXPower_eq_C_add_X_mul_dropXPower_succ {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (p : CPolynomial F) (depth : ℕ) : p.dropXPower depth = CPolynomial.C (p.coeff depth) + CPolynomial.X * p.dropXPower (depth + 1)

theorem CompPoly.GuruswamiSudan.polynomial_monomial_substitution_term {F : Type u_1} [Field F] (a coeff : F) (p : Polynomial F) (x y t : ℕ) : (Polynomial.monomial x) coeff * ((Polynomial.X * p) ^ t * Polynomial.C a ^ (y - t) * Polynomial.C ↑(y.choose t)) = (Polynomial.monomial (x + t)) (coeff * ↑(y.choose t) * a ^ (y - t)) * p ^ t

theorem CompPoly.GuruswamiSudan.polynomial_monomial_substitution_sum {F : Type u_1} [Field F] (a coeff : F) (p : Polynomial F) (x y : ℕ) : ∑ t ∈ Finset.range (y + 1), (Polynomial.monomial (x + t)) (coeff * ↑(y.choose t) * a ^ (y - t)) * p ^ t = (Polynomial.monomial x) coeff * (Polynomial.C a + Polynomial.X * p) ^ y

theorem CompPoly.GuruswamiSudan.foldl_cpoly_toPoly_add {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (f : ℕ → CPolynomial F) (xs : List ℕ) (acc : CPolynomial F) (accPoly : Polynomial F) : acc.toPoly = accPoly → (List.foldl (fun (acc : CPolynomial F) (x : ℕ) => acc + f x) acc xs).toPoly = List.foldl (fun (acc : Polynomial F) (x : ℕ) => acc + (f x).toPoly) accPoly xs

theorem CompPoly.GuruswamiSudan.cpoly_monomial_substitution_sum {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (a coeff : F) (p : CPolynomial F) (x y : ℕ) : List.foldl (fun (acc : CPolynomial F) (t : ℕ) => acc + CPolynomial.monomial (x + t) (coeff * ↑(y.choose t) * a ^ (y - t)) * p ^ t) 0 (List.range' 0 (y + 1)) = CPolynomial.monomial x coeff * (CPolynomial.C a + CPolynomial.X * p) ^ y