fix 1/2

Author: MrBrain295

ArkLib/Data/MvPolynomial/SchwartzZippelCounting.lean

@@ -141,3 +141,43 @@ lemma prob_eval_zero_le_div
     · convert congr_arg₂ (· * ·) (card_filter_eval_subtype_eq_piFinset S f) rfl
     · rw [Fintype.card_pi]
       aesop
+
+section ZeroCount
+
+open Finset
+
+/-- Counting Schwartz-Zippel over all of a finite field: a nonzero polynomial in `s` variables of
+total degree at most `D` has at most `D * |F| ^ (s - 1)` zeros in `Fin s → F`. -/
+theorem MvPolynomial.card_zeros_le_of_totalDegree_le_fin
+    {F : Type*} [Field F] [Fintype F] [DecidableEq F] {s : ℕ}
+    (f : MvPolynomial (Fin s) F) (hf : f ≠ 0) {D : ℕ} (hd : f.totalDegree ≤ D) :
+    #{x : Fin s → F | MvPolynomial.eval x f = 0} ≤ D * Fintype.card F ^ (s - 1) := by
+  classical
+  have hq : 0 < Fintype.card F := Fintype.card_pos
+  have key := schwartz_zippel_counting f hf (fun _ => Finset.univ) D (Fintype.card F) hd hq
+    (fun i => by simp)
+  simp only [Fintype.piFinset_univ, Finset.card_univ, Finset.prod_const] at key
+  match s with
+  | 0 => simpa using le_trans (Nat.le_mul_of_pos_right _ hq) (by simpa using key)
+  | (t + 1) =>
+    refine Nat.le_of_mul_le_mul_right ?_ hq
+    simpa [pow_succ, mul_assoc] using key
+
+/-- Counting Schwartz-Zippel over all of a finite field, for an arbitrary finite index type of
+variables: a nonzero polynomial in the variables `ι` of total degree at most `D` has at most
+`D * |F| ^ (|ι| - 1)` zeros in `ι → F`. -/
+theorem MvPolynomial.card_zeros_le_of_totalDegree_le
+    {F : Type*} [Field F] [Fintype F] [DecidableEq F] {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (f : MvPolynomial ι F) (hf : f ≠ 0) {D : ℕ} (hd : f.totalDegree ≤ D) :
+    #{x : ι → F | MvPolynomial.eval x f = 0} ≤ D * Fintype.card F ^ (Fintype.card ι - 1) := by
+  classical
+  set e := Fintype.equivFin ι
+  have hg : MvPolynomial.rename (e : ι → Fin (Fintype.card ι)) f ≠ 0 := fun h =>
+    hf (MvPolynomial.rename_injective _ e.injective (by simpa using h))
+  have hgd : (MvPolynomial.rename (e : ι → Fin (Fintype.card ι)) f).totalDegree ≤ D :=
+    le_trans (MvPolynomial.totalDegree_rename_le _ _) hd
+  refine le_trans (le_of_eq ?_) (MvPolynomial.card_zeros_le_of_totalDegree_le_fin _ hg hgd)
+  refine Finset.card_nbij' (fun x => x ∘ e.symm) (fun y => y ∘ e) ?_ ?_ ?_ ?_ <;>
+    intro x hx <;> simp_all [MvPolynomial.eval_rename, Function.comp_assoc]
+
+end ZeroCount