Alon's Combinatorial Nullstellensatz #
This is a formalization of Noga Alon's Combinatorial Nullstellensatz. It follows [Alo99].
We consider a family S : σ → Finset R
of finite subsets of a domain R
and a multivariate polynomial f
in MvPolynomial σ R
.
The combinatorial Nullstellensatz gives combinatorial constraints for
the vanishing of f
at any x : σ → R
such that x s ∈ S s
for all s
.
MvPolynomial.eq_zero_of_eval_zero_at_prod_finset
: iff
vanishes at any such point andf.degreeOf s < #(S s)
for alls
, thenf = 0
.combinatorial_nullstellensatz_exists_linearCombination
Iff
vanishes at every such point, then it can be written as a linear combinationf = linearCombination (MvPolynomial σ R) (fun i ↦ ∏ r ∈ S i, (X i - C r)) h
, for someh : σ →₀ MvPolynomial σ R
such that((∏ r ∈ S s, (X i - C r)) * h i).totalDegree ≤ f.totalDegree
for alls
.combinatorial_nullstellensatz_exists_eval_nonzero
a multi-indext : σ →₀ ℕ
such thatt s < (S s).card
for alls
,f.totalDegree = t.degree
andf.coeff t ≠ 0
, there exists a pointx : σ → R
such thatx s ∈ S s
for alls
andf.eval s ≠ 0
.
TODO #
- Applications
- relation with Schwartz–Zippel lemma, as in [Rot23]
References #
A multivariate polynomial that vanishes on a large product finset is the zero polynomial.
The Combinatorial Nullstellensatz.
If f
vanishes at every point x : σ → R
such that x s ∈ S s
for all s
,
then it can be written as a linear combination
f = linearCombination (MvPolynomial σ R) (fun i ↦ (∏ r ∈ S i, (X i - C r))) h
,
for some h : σ →₀ MvPolynomial σ R
such that
((∏ r ∈ S s, (X i - C r)) * h i).totalDegree ≤ f.totalDegree
for all s
.
[Alo99], theorem 1.
The Combinatorial Nullstellensatz.
Given a multi-index t : σ →₀ ℕ
such that t s < (S s).card
for all s
,
f.totalDegree = t.degree
and f.coeff t ≠ 0
,
there exists a point x : σ → R
such that x s ∈ S s
for all s
and f.eval s ≠ 0
.
[Alo99], theorem 2