Sums of low-degree polynomials over the units of a finite field

Let K be a finite field with q elements. A polynomial of degree less than q - 1 sums to zero over K, so its sum over the units Kˣ is minus its value at 0. Restricting a multivariate polynomial to the line u ↦ u • τ + x turns this into the identity that removes the masks τ from masked evaluations of a low-degree polynomial: the sum over all units u of p (u • τ + x) is -p x.

This is the algebraic core of the Cook–Mertz Tree Evaluation algorithm, there phrased with powers of a primitive root of unity of order q - 1, which run through the units.

Main results

• FiniteField.sum_eval_eq_zero_of_natDegree_lt: a polynomial of degree less than q - 1 sums to zero over K.
• FiniteField.sum_units_eval: its sum over Kˣ is minus its value at 0.
• FiniteField.natDegree_eval₂_line_le: restricting a multivariate polynomial to a line gives a univariate polynomial of degree at most the total degree.
• FiniteField.eval_eval₂_line: evaluating the univariate line restriction at t evaluates the multivariate polynomial at t • τ + x.
• FiniteField.sum_units_eval_mul_add: for a multivariate polynomial of total degree less than q - 1, ∑ u : Kˣ, p (u • τ + x) = -p x.

References

• J. Cook and I. Mertz, Tree Evaluation is in Space O(log n · log log n), Corollary 9 and Lemma 12.
• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure, Equation (3).

theorem FiniteField.sum_eval_eq_zero_of_natDegree_lt {K : Type u_1} [Field K] [Fintype K] {g : Polynomial K} (hg : g.natDegree < Fintype.card K - 1) : ∑ x : K, Polynomial.eval x g = 0

A polynomial of degree less than q - 1 sums to zero over the field.

theorem FiniteField.sum_units_eval {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {g : Polynomial K} (hg : g.natDegree < Fintype.card K - 1) : ∑ u : Kˣ, Polynomial.eval (↑u) g = -Polynomial.eval 0 g

A polynomial of degree less than q - 1 sums over the units to minus its value at 0.

theorem FiniteField.natDegree_eval₂_line_le {K : Type u_1} [Field K] {ι : Type u_2} (p : MvPolynomial ι K) (τ x : ι → K) : (MvPolynomial.eval₂ Polynomial.C (fun (i : ι) => Polynomial.C (τ i) * Polynomial.X + Polynomial.C (x i)) p).natDegree ≤ p.totalDegree

Restricting a multivariate polynomial to the line t ↦ t • τ + x gives a univariate polynomial of degree at most the total degree.

theorem FiniteField.eval_eval₂_line {K : Type u_1} [Field K] {ι : Type u_2} (p : MvPolynomial ι K) (τ x : ι → K) (t : K) : Polynomial.eval t (MvPolynomial.eval₂ Polynomial.C (fun (i : ι) => Polynomial.C (τ i) * Polynomial.X + Polynomial.C (x i)) p) = (MvPolynomial.eval fun (i : ι) => t * τ i + x i) p

Evaluating the univariate restriction of p to the line t ↦ t • τ + x at t evaluates p at i ↦ t * τ i + x i.

theorem FiniteField.sum_units_eval_mul_add {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ι : Type u_2} {p : MvPolynomial ι K} (hp : p.totalDegree < Fintype.card K - 1) (τ x : ι → K) : ∑ u : Kˣ, (MvPolynomial.eval fun (i : ι) => ↑u * τ i + x i) p = -(MvPolynomial.eval x) p

Unmasking low-degree polynomials. If p has total degree less than q - 1, then summing the masked evaluations p (u • τ + x) over all units u gives -p x, for every mask τ.