Degree bounds for Polishchuk-Spielman

This file contains auxiliary lemmas regarding degree bounds, evaluation, and variable swapping for bivariate polynomials, used in the Polishchuk-Spielman lemma [BCIKS20].

Main results

• ps_bx_lt_nx, ps_by_lt_ny: Bounds on the degrees parameters.
• ps_card_eval_x_eq_zero_le_degree_x, ps_card_eval_y_eq_zero_le_nat_degree_y: Bounds on the number of roots of a bivariate polynomial on lines.
• ps_eval_y_eq_eval_x_swap: Relates evaluation in Y to evaluation in X of the swapped polynomial.
• ps_exists_x_preserve_nat_degree_y, ps_exists_y_preserve_degree_x: Existence of evaluation points preserving the degree.

References

• [Ben-Sasson, E., Carmon, D., Ishai, Y., Kopparty, S., and Saraf, S., Proximity Gaps for Reed-Solomon Codes][BCIKS20]

theorem ps_bx_lt_nx {b_x b_y : ℕ} {n_x n_y : ℕ+} (h_le_1 : 1 > ↑b_x / ↑↑n_x + ↑b_y / ↑↑n_y) : b_x < ↑n_x

theorem ps_by_lt_ny {b_x b_y : ℕ} {n_x n_y : ℕ+} (h_le_1 : 1 > ↑b_x / ↑↑n_x + ↑b_y / ↑↑n_y) : b_y < ↑n_y

theorem ps_card_eval_x_eq_zero_le_degree_x {F : Type} [Field F] [DecidableEq F] (A : Polynomial (Polynomial F)) (hA : A ≠ 0) (P : Finset F) : {x ∈ P | Polynomial.Bivariate.evalX x A = 0}.card ≤ Polynomial.Bivariate.degreeX A

theorem ps_card_eval_y_eq_zero_le_nat_degree_y {F : Type} [Field F] [DecidableEq F] (A : Polynomial (Polynomial F)) (hA : A ≠ 0) (P : Finset F) : {y ∈ P | Polynomial.Bivariate.evalY y A = 0}.card ≤ Polynomial.Bivariate.natDegreeY A

theorem ps_coeff_mul_monomial_ite {R : Type} [Semiring R] (A : Polynomial R) (j i : ℕ) (r : R) : (A * (Polynomial.monomial j) r).coeff i = if j ≤ i then A.coeff (i - j) * r else 0

theorem ps_coeff_mul_sum_monomial {R : Type} [CommRing R] (A : Polynomial R) (m n : ℕ) (hm : A.natDegree ≤ m) (c : Fin n → R) (i : ℕ) : (A * ∑ j : Fin n, (Polynomial.monomial ↑j) (c j)).coeff i = ∑ j : Fin n, if ↑j ≤ i ∧ i ≤ ↑j + m then A.coeff (i - ↑j) * c j else 0

theorem ps_degree_x_swap {F : Type} [CommRing F] (f : Polynomial (Polynomial F)) : Polynomial.Bivariate.degreeX (Polynomial.Bivariate.swap f) = Polynomial.Bivariate.natDegreeY f

theorem ps_descend_eval_x {F : Type} [Field F] [DecidableEq F] {A B G A1 B1 : Polynomial (Polynomial F)} (hA : A = G * A1) (hB : B = G * B1) (x : F) (hx : Polynomial.Bivariate.evalX x G ≠ 0) (q : Polynomial F) (h : Polynomial.Bivariate.evalX x B = q * Polynomial.Bivariate.evalX x A) : Polynomial.Bivariate.evalX x B1 = q * Polynomial.Bivariate.evalX x A1

theorem ps_descend_eval_y {F : Type} [Field F] [DecidableEq F] {A B G A1 B1 : Polynomial (Polynomial F)} (hA : A = G * A1) (hB : B = G * B1) (y : F) (hy : Polynomial.Bivariate.evalY y G ≠ 0) (q : Polynomial F) (h : Polynomial.Bivariate.evalY y B = q * Polynomial.Bivariate.evalY y A) : Polynomial.Bivariate.evalY y B1 = q * Polynomial.Bivariate.evalY y A1

theorem ps_eval_x_eq_map {F : Type} [CommSemiring F] (x : F) (f : Polynomial (Polynomial F)) : Polynomial.Bivariate.evalX x f = Polynomial.map (Polynomial.evalRingHom x) f

theorem ps_eval_y_eq_eval_x_swap {F : Type} [CommRing F] (y : F) (f : Polynomial (Polynomial F)) : Polynomial.Bivariate.evalY y f = Polynomial.Bivariate.evalX y (Polynomial.Bivariate.swap f)

theorem ps_exists_x_preserve_nat_degree_y {F : Type} [Field F] [DecidableEq F] (B : Polynomial (Polynomial F)) (hB : B ≠ 0) (P_x : Finset F) (hcard : P_x.card > Polynomial.Bivariate.degreeX B) : ∃ x ∈ P_x, (Polynomial.Bivariate.evalX x B).natDegree = Polynomial.Bivariate.natDegreeY B

theorem ps_exists_y_preserve_degree_x {F : Type} [Field F] [DecidableEq F] (B : Polynomial (Polynomial F)) (hB : B ≠ 0) (P_y : Finset F) (hcard : P_y.card > Polynomial.Bivariate.natDegreeY B) : ∃ y ∈ P_y, (Polynomial.Bivariate.evalY y B).natDegree = Polynomial.Bivariate.degreeX B

theorem ps_degree_bounds_of_mul {F : Type} [Field F] (a_x a_y b_x b_y : ℕ) (n_x n_y : ℕ+) (h_bx_ge_ax : b_x ≥ a_x) (h_by_ge_ay : b_y ≥ a_y) {A B P : Polynomial (Polynomial F)} (hA : A ≠ 0) (hBA : B = P * A) (h_f_degX : a_x ≥ Polynomial.Bivariate.degreeX A) (h_f_degY : a_y ≥ Polynomial.Bivariate.natDegreeY A) (h_g_degY : b_y ≥ Polynomial.Bivariate.natDegreeY B) (P_x P_y : Finset F) [Nonempty ↥P_x] [Nonempty ↥P_y] (quot_x quot_y : F → Polynomial F) (h_card_Px : ↑n_x ≤ P_x.card) (h_card_Py : ↑n_y ≤ P_y.card) (h_quot_x : ∀ y ∈ P_y, (quot_x y).natDegree ≤ b_x - a_x ∧ Polynomial.Bivariate.evalY y B = quot_x y * Polynomial.Bivariate.evalY y A) (h_quot_y : ∀ x ∈ P_x, (quot_y x).natDegree ≤ b_y - a_y ∧ Polynomial.Bivariate.evalX x B = quot_y x * Polynomial.Bivariate.evalX x A) (h_le_1 : 1 > ↑b_x / ↑↑n_x + ↑b_y / ↑↑n_y) : Polynomial.Bivariate.degreeX P ≤ b_x - a_x ∧ Polynomial.Bivariate.natDegreeY P ≤ b_y - a_y

theorem ps_gcd_decompose {F : Type} [Field F] {A B : Polynomial (Polynomial F)} (hA : A ≠ 0) (hB : B ≠ 0) : ∃ (G : Polynomial (Polynomial F)) (A1 : Polynomial (Polynomial F)) (B1 : Polynomial (Polynomial F)), A = G * A1 ∧ B = G * B1 ∧ IsRelPrime A1 B1 ∧ A1 ≠ 0 ∧ B1 ≠ 0

theorem ps_is_rel_prime_swap {F : Type} [CommRing F] {A B : Polynomial (Polynomial F)} (h : IsRelPrime A B) : IsRelPrime (Polynomial.Bivariate.swap A) (Polynomial.Bivariate.swap B)

theorem ps_nat_degree_y_swap {F : Type} [CommRing F] (f : Polynomial (Polynomial F)) : Polynomial.Bivariate.natDegreeY (Polynomial.Bivariate.swap f) = Polynomial.Bivariate.degreeX f