The Schwartz-Zippel lemma

This file contains a proof of the Schwartz-Zippel lemma.

This lemma tells us that the probability that a nonzero multivariable polynomial over an integral domain evaluates to zero at a random point is bounded by the degree of the polynomial over the size of the field, or more generally, that a nonzero multivariable polynomial over any integral domain has a low probability of being zero when evaluated at points drawn at random from some finite subset of the field. This lemma is useful as a probabilistic polynomial identity test.

Main results

• MvPolynomial.schwartz_zippel_sup_sum: Sharper version of Schwartz-Zippel for a dependent product of sets S i, with the RHS being the supremum of ∑ i, degᵢ s / #(S i) ranging over monomials s of the polynomial.
• MvPolynomial.schwartz_zippel_sum_degreeOf: Schwartz-Zippel for a dependent product of sets S i, with the RHS being the sum of degᵢ p / #(S i).
• MvPolynomial.schwartz_zippel_totalDegree: Nondependent version of schwartz_zippel_sup_sum, with the RHS being p.totalDegree / #S.

TODO

• Generalize to polynomials over arbitrary variable types
• Prove the stronger statement that one can replace the degrees of p in the RHS by the degrees of the maximal monomial of p in some lexicographic order.
• Write a tactic to apply this lemma to a given polynomial

References

• [DeML78]
• [Sch80]
• [Zip79]

theorem MvPolynomial.schwartz_zippel_sup_sum {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R) : ↑(Finset.filter (fun (x : Fin n → R) => (MvPolynomial.eval x) p = 0) (Fintype.piFinset fun (i : Fin n) => S i)).card / ∏ i : Fin n, ↑(S i).card ≤ p.support.sup fun (s : Fin n →₀ ℕ) => ∑ i : Fin n, ↑(s i) / ↑(S i).card

The Schwartz-Zippel lemma

For a nonzero multivariable polynomial p over an integral domain, the probability that p evaluates to zero at points drawn at random from a product of finite subsets S i of the integral domain is bounded by the supremum of ∑ i, degᵢ s / #(S i) ranging over monomials s of p.

theorem MvPolynomial.schwartz_zippel_sum_degreeOf {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R) : ↑(Finset.filter (fun (x : Fin n → R) => (MvPolynomial.eval x) p = 0) (Fintype.piFinset fun (i : Fin n) => S i)).card / ∏ i : Fin n, ↑(S i).card ≤ ∑ i : Fin n, ↑(MvPolynomial.degreeOf i p) / ↑(S i).card

The Schwartz-Zippel lemma

For a nonzero multivariable polynomial p over an integral domain, the probability that p evaluates to zero at points drawn at random from a product of finite subsets S i of the integral domain is bounded by the sum of degᵢ p / #(S i).

theorem MvPolynomial.schwartz_zippel_totalDegree {R : Type u_1} [CommRing R] [IsDomain R] [DecidableEq R] {n : ℕ} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Finset R) : ↑(Finset.filter (fun (f : Fin n → R) => (MvPolynomial.eval f) p = 0) (Fintype.piFinset fun (x : Fin n) => S)).card / ↑S.card ^ n ≤ ↑p.totalDegree / ↑S.card

The Schwartz-Zippel lemma

For a nonzero multivariable polynomial p over an integral domain, the probability that p evaluates to zero at points drawn at random from some finite subset S of the integral domain is bounded by the degree of p over #S. This version presents this lemma in terms of Finset.