English
For a nonzero polynomial p, the Schwartz-Zippel bound via degreeOf holds: the zeros bound is at most the sum over variables of deg_i(p)/|S_i|.
Русский
Для не нуль-го многочлена p справедлива оценка Шварца-Циппеля через deg_i(p): число нулевых значений ограничено суммой по переменным deg_i(p)/|S_i|.
LaTeX
$$$ #\{x : eval x p = 0\} / ∏ i #(S_i) \le \sum_i (p.\degreeOf i / #(S_i)) $$$
Lean4
/-- 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 schwartz_zippel_sum_degreeOf {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Fin n → Finset R) :
#({x ∈ S ^^ n | eval x p = 0}) / ∏ i, (#(S i) : ℚ≥0) ≤ ∑ i, (p.degreeOf i / #(S i) : ℚ≥0) := by
calc
_ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := schwartz_zippel_sup_sum hp S
_ ≤ ∑ i, (p.degreeOf i / #(S i) : ℚ≥0) := Finset.sup_le fun s hs ↦ by gcongr with i; exact monomial_le_degreeOf i hs
