-- Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean
/-- 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`. -/
lemma 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)

Proof state:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = (p.support.sup fun i => ↑(i.sum fun x e => e)) / ↑(#S)

Tactic:
rw [sup_div₀ (ha := show 0 < (#S : ℚ≥0) by positivity)]

Result:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = p.support.sup fun i => ↑(i.sum fun x e => e) / ↑(#S)

Proof state:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = p.support.sup fun i => ↑(i.sum fun x e => e) / ↑(#S)

Tactic:
simp [← sum_div, Finsupp.sum_fintype]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ 0 < ↑(#S)

Tactic:
positivity

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)

Tactic:
simp

Result:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s => 0) = 0

Proof state:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s => 0) = 0

Tactic:
simp only [← _root_.bot_eq_zero, sup_bot]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ ↑(#(filter (fun f => (eval f) p = 0) (piFinset fun x => S))) / ↑(#S) ^ n =
    ↑(#(filter (fun f => (eval f) p = 0) (piFinset fun x => S))) / ∏ i : Fin n, ↑(#S)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
obtain rfl | hs := S.eq_empty_or_nonempty

Result:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)

case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Proof state:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = ↑p.totalDegree / ↑(#S)

Tactic:
simp_rw [totalDegree, Nat.cast_finsetSup]

Result:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s => ∑ i : Fin n, ↑(s i) / ↑(#S)) = (p.support.sup fun i => ↑(i.sum fun x e => e)) / ↑(#S)