Existence of polynomials for Polishchuk-Spielman

This file contains the core existence proofs for the polynomials $P$ and $Q$ required by the Polishchuk-Spielman lemma [BCIKS20].

Main results

• ps_exists_p: Existence of a polynomial P such that B = P * A.
• ps_exists_qx_of_cancel: Existence of Q_x after cancellation in the X direction.
• ps_exists_qy_of_cancel: Existence of Q_y after cancellation in the Y direction.

References

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

theorem ps_exists_p_of_degree_x_eq_zero_nat_degree_y_eq_zero {F : Type} [Field F] {A B : Polynomial (Polynomial F)} (hA0 : A ≠ 0) (hdegX : Polynomial.Bivariate.degreeX A = 0) (hdegY : Polynomial.Bivariate.natDegreeY A = 0) : ∃ (P : Polynomial (Polynomial F)), B = P * A

theorem ps_exists_qx_of_cancel {F : Type} [Field F] [DecidableEq F] (a_x : ℕ) (n_x : ℕ+) {A B P : Polynomial (Polynomial F)} (hA : A ≠ 0) (hBA : B = P * A) (P_x : Finset F) (h_card_Px : ↑n_x ≤ P_x.card) (quot_y : F → Polynomial F) (h_quot_y : ∀ x ∈ P_x, Polynomial.Bivariate.evalX x B = quot_y x * Polynomial.Bivariate.evalX x A) (h_f_degX : a_x ≥ Polynomial.Bivariate.degreeX A) : ∃ (Q_x : Finset F), Q_x.card ≥ ↑n_x - a_x ∧ Q_x ⊆ P_x ∧ ∀ x ∈ Q_x, Polynomial.Bivariate.evalX x P = quot_y x

theorem ps_exists_qy_of_cancel {F : Type} [Field F] [DecidableEq F] (a_y : ℕ) (n_y : ℕ+) {A B P : Polynomial (Polynomial F)} (hA : A ≠ 0) (hBA : B = P * A) (P_y : Finset F) (h_card_Py : ↑n_y ≤ P_y.card) (quot_x : F → Polynomial F) (h_quot_x : ∀ y ∈ P_y, Polynomial.Bivariate.evalY y B = quot_x y * Polynomial.Bivariate.evalY y A) (h_f_degY : a_y ≥ Polynomial.Bivariate.natDegreeY A) : ∃ (Q_y : Finset F), Q_y.card ≥ ↑n_y - a_y ∧ Q_y ⊆ P_y ∧ ∀ y ∈ Q_y, Polynomial.Bivariate.evalY y P = quot_x y

theorem ps_coprime_case_constant {F : Type} [Field F] [DecidableEq 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 : Polynomial (Polynomial F)) (hA0 : A ≠ 0) (hB0 : B ≠ 0) (hrel : IsRelPrime A B) (h_f_degX : a_x ≥ Polynomial.Bivariate.degreeX A) (h_g_degX : b_x ≥ Polynomial.Bivariate.degreeX B) (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 A = 0 ∧ Polynomial.Bivariate.natDegreeY A = 0

theorem ps_exists_p_nonzero {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 : Polynomial (Polynomial F)) (hA0 : A ≠ 0) (hB0 : B ≠ 0) (h_f_degX : a_x ≥ Polynomial.Bivariate.degreeX A) (h_g_degX : b_x ≥ Polynomial.Bivariate.degreeX B) (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) : ∃ (P : Polynomial (Polynomial F)), B = P * A

theorem ps_exists_p {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 : Polynomial (Polynomial F)) (h_f_degX : a_x ≥ Polynomial.Bivariate.degreeX A) (h_g_degX : b_x ≥ Polynomial.Bivariate.degreeX B) (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) : ∃ (P : Polynomial (Polynomial F)), B = P * A