Shifting a low-individual-degree polynomial along an axis

Let g be a polynomial in n variables of individual degree at most d over a finite field F with q elements, given by its coefficient vector, and suppose g has a nonzero coefficient on a monomial ∏ₖ Xₖ^(eₖ) containing Xᵢ (eᵢ ≠ 0). Then g changes value along most axis-parallel steps in direction i: g(u + t eᵢ) ≠ g(u) for at least q^n (q - (n + 1) d) of the pairs (u, t) ∈ F^n × F (card_shift_ne_ge).

The proof restricts g to the axis-parallel line through u in direction i: a univariate polynomial g.onAxis i u of degree at most d in the i-th coordinate, whose coefficients are the coefficient vectors g.coef {i} t evaluated at u. Its coefficient on X^(eᵢ) is a nonzero coefficient vector G evaluated at u. Where G(u) ≠ 0 the restriction is nonconstant, so it takes the value g(u) at most d times (card_shift_eq_le); and by Schwartz--Zippel (card_eval_eq_zero_le) G(u) = 0 for at most n d q^(n - 1) points u.

noncomputable def MIPRE.LIDT.LowIndDegPoly.onAxis {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) : Polynomial F

The restriction of g to the axis-parallel line through u in direction i, as a univariate polynomial in the i-th coordinate: its value at u i + t is g(u + t eᵢ).

Equations

• g.onAxis i u = ∑ t : Fin n → Fin (d + 1), Polynomial.C ((g.coef {i} t).eval u) * Polynomial.X ^ ↑(t i)

theorem MIPRE.LIDT.LowIndDegPoly.eval_onAxis {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) (x : F) : Polynomial.eval x (g.onAxis i u) = ∑ t : Fin n → Fin (d + 1), (g.coef {i} t).eval u * x ^ ↑(t i)

Evaluation of the restriction to an axis-parallel line.

theorem MIPRE.LIDT.LowIndDegPoly.eval_shift_eq_eval_onAxis {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) (t : F) : g.eval (u + t • Pi.single i 1) = Polynomial.eval (u i + t) (g.onAxis i u)

Along the axis-parallel line through u in direction i, g is its restriction.

theorem MIPRE.LIDT.LowIndDegPoly.eval_eq_eval_onAxis {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) : g.eval u = Polynomial.eval (u i) (g.onAxis i u)

At u itself, g is its restriction evaluated at u i.

theorem MIPRE.LIDT.LowIndDegPoly.natDegree_onAxis_le {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) : (g.onAxis i u).natDegree ≤ d

The restriction to an axis-parallel line has degree at most d.

theorem MIPRE.LIDT.LowIndDegPoly.coeff_onAxis {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) (u : Point F n) (e : Fin n → Fin (d + 1)) : (g.onAxis i u).coeff ↑(e i) = (g.coef {i} (maskOn {i} e)).eval u

The coefficient of X^(e i) in the restriction is the coefficient vector of the pattern Xᵢ^(e i), evaluated at u.

theorem MIPRE.LIDT.card_shift_eq_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (g : LowIndDegPoly) {i : Fin n} {e : Fin n → Fin (d + 1)} (hi : ↑(e i) ≠ 0) {u : Point F n} (hu : (g.coef {i} (maskOn {i} e)).eval u ≠ 0) : {t : F | g.eval (u + t • Pi.single i 1) = g.eval u}.card ≤ d

Where the coefficient vector of the pattern Xᵢ^(e i), e i ≠ 0, does not vanish at u, g takes the value g(u) at most d times along the axis-parallel line through u in direction i.

theorem MIPRE.LIDT.card_pairs_shift_eq_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (g : LowIndDegPoly) {i : Fin n} {e : Fin n → Fin (d + 1)} (he : g e ≠ 0) (hi : ↑(e i) ≠ 0) : ↑{p : Point F n × F | g.eval (p.1 + p.2 • Pi.single i 1) = g.eval p.1}.card ≤ (↑n + 1) * ↑d * ↑(Fintype.card F) ^ n

The pairs along which g does not change: if g has a nonzero coefficient on a monomial containing Xᵢ, then g(u + t eᵢ) = g(u) for at most (n + 1) d q^n of the pairs (u, t).

theorem MIPRE.LIDT.card_shift_ne_ge {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n d : ℕ} (g : LowIndDegPoly) {i : Fin n} {e : Fin n → Fin (d + 1)} (he : g e ≠ 0) (hi : ↑(e i) ≠ 0) : ↑(Fintype.card F) ^ n * (↑(Fintype.card F) - (↑n + 1) * ↑d) ≤ ↑{p : Point F n × F | g.eval (p.1 + p.2 • Pi.single i 1) ≠ g.eval p.1}.card

Shifts along an axis change a polynomial that depends on the axis variable: if g has a nonzero coefficient on a monomial containing Xᵢ, then g(u + t eᵢ) ≠ g(u) for at least q^n (q - (n + 1) d) of the pairs (u, t) ∈ F^n × F.