English
A total-degree bound version of Schwartz-Zippel: the probability that p evaluates to zero is at most p.totalDegree / |S| when evaluating on a finite set S.
Русский
Версия леммы Шварца-Циппеля через общую степень: вероятность того, что p обнуляется при произвольном выборе значений из конечного множества S, не больше p.totalDegree / |S|.
LaTeX
$$$ #\{f \in piFinset (fun _ => S) : eval f p = 0\} / (#S ^ n : \mathbb{Q}_{\ge 0}) \le p.totalDegree / #S $$$
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 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`. -/
theorem schwartz_zippel_totalDegree {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0) (S : Finset R) :
#({f ∈ piFinset fun _ ↦ S | eval f p = 0}) / (#S ^ n : ℚ≥0) ≤ p.totalDegree / #S :=
calc
_ = #({f ∈ piFinset fun _ ↦ S | eval f p = 0}) / (∏ i : Fin n, #S : ℚ≥0) := by simp
_ ≤ p.support.sup fun s ↦ ∑ i, (s i / #S : ℚ≥0) := (schwartz_zippel_sup_sum hp _)
_ = p.totalDegree / #S := by
obtain rfl | hs := S.eq_empty_or_nonempty
· simp
simp only [← _root_.bot_eq_zero, sup_bot]
simp_rw [totalDegree, Nat.cast_finsetSup]
rw [sup_div₀ (ha := show 0 < (#S : ℚ≥0) by positivity)]
simp [← sum_div, Finsupp.sum_fintype]
