English
For a multivariate polynomial f over a finite field with total degree bound, the sum of evaluations over the full grid vanishes.
Русский
Для многочлена f над сконечной полем, сумма значений f на всех точках нулевая при ограничении степени.
LaTeX
$$$\\sum_{x} \\mathrm{eval}(x,f) = 0$ under the specified degree bound.$$
Lean4
theorem sum_eval_eq_zero (f : MvPolynomial σ K) (h : f.totalDegree < (q - 1) * Fintype.card σ) : ∑ x, eval x f = 0 :=
by
haveI : DecidableEq K := Classical.decEq K
calc
∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by simp only [eval_eq']
_ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
_ = 0 := sum_eq_zero ?_
intro d hd
obtain ⟨i, hi⟩ : ∃ i, d i < q - 1 := f.exists_degree_lt (q - 1) h hd
calc
(∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i) = f.coeff d * ∑ x : σ → K, ∏ i, x i ^ d i := (mul_sum ..).symm
_ = 0 := (mul_eq_zero.mpr ∘ Or.inr) ?_
calc
(∑ x : σ → K, ∏ i, x i ^ d i) =
∑ x₀ : { j // j ≠ i } → K, ∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j :=
(Fintype.sum_fiberwise _ _).symm
_ = 0 := Fintype.sum_eq_zero _ ?_
intro x₀
let e : K ≃ { x // x ∘ ((↑) : _ → σ) = x₀ } := (Equiv.subtypeEquivCodomain _).symm
calc
(∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j) = ∑ a : K, ∏ j : σ, (e a : σ → K) j ^ d j :=
(e.sum_comp _).symm
_ = ∑ a : K, (∏ j, x₀ j ^ d j) * a ^ d i := (Fintype.sum_congr _ _ ?_)
_ = (∏ j, x₀ j ^ d j) * ∑ a : K, a ^ d i := by rw [mul_sum]
_ = 0 := by rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]
intro a
let e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl _
letI : Unique { j // j = i } :=
{ default := ⟨i, rfl⟩
uniq := fun ⟨j, h⟩ => Subtype.val_injective h }
calc
(∏ j : σ, (e a : σ → K) j ^ d j) = (e a : σ → K) i ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by
rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl
_ = a ^ d i * ∏ j : { j // j ≠ i }, (e a : σ → K) j ^ d j := by rw [Equiv.subtypeEquivCodomain_symm_apply_eq]
_ = a ^ d i * ∏ j, x₀ j ^ d j := (congr_arg _ (Fintype.prod_congr _ _ ?_))
_ = (∏ j, x₀ j ^ d j) * a ^ d i :=
mul_comm _
_
-- the remaining step of the calculation above
rintro ⟨j, hj⟩
change (e a : σ → K) j ^ d j = x₀ ⟨j, hj⟩ ^ d j
rw [Equiv.subtypeEquivCodomain_symm_apply_ne]
