Polynomial preliminaries

Packages the paper's low-individual-degree polynomial class together with Schwartz-Zippel bounds as thin wrappers around Mathlib's existing multivariate polynomial theorems.

References

• references/ldt-paper/preliminaries.tex, Section 3 (Preliminaries)

@[reducible, inline]

noncomputable abbrev MIPStarRE.LDT.Preliminaries.polyFunc (m : ℕ) (K : Type u_1) [CommSemiring K] (d : ℕ) : Submodule K (MvPolynomial (Fin m) K)

\polyfunc{m}{q}{d} from the paper's definition of low-individual-degree polynomials. This is Mathlib's MvPolynomial.restrictDegree submodule.

Equations

• MIPStarRE.LDT.Preliminaries.polyFunc m K d = MvPolynomial.restrictDegree (Fin m) K d

theorem MIPStarRE.LDT.Preliminaries.degreeOf_le_of_mem_polyFunc {m d : ℕ} {K : Type u_1} [CommSemiring K] {p : MvPolynomial (Fin m) K} (hp : p ∈ polyFunc m K d) (i : Fin m) : MvPolynomial.degreeOf i p ≤ d

If p ∈ polyFunc m K d, then p.degreeOf i ≤ d for every variable i.

theorem MIPStarRE.LDT.Preliminaries.polyFuncMonotone {m d : ℕ} {K : Type u_1} [CommSemiring K] : polyFunc m K d ≤ polyFunc m K (d + 1)

Paper label rem:individual-degree-convention.

Increasing the individual-degree bound enlarges the corresponding low-degree polynomial class.

noncomputable def MIPStarRE.LDT.Preliminaries.polynomialAgreementProbability (m : ℕ) (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (g h : MvPolynomial (Fin m) K) : ℚ≥0

The uniform agreement probability of two polynomials on K^m, written as a finite cardinality ratio over K^m.

Equations

• MIPStarRE.LDT.Preliminaries.polynomialAgreementProbability m K g h = ↑{x : Fin m → K | (MvPolynomial.eval x) g = (MvPolynomial.eval x) h}.card / ↑(Fintype.card K) ^ m

theorem MIPStarRE.LDT.Preliminaries.totalDegree_le_mul_of_degreeOf_le {m d : ℕ} {K : Type u_1} [CommSemiring K] {p : MvPolynomial (Fin m) K} (hdeg : ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d) : p.totalDegree ≤ m * d

If every individual degree of p is at most d, then the total degree of p is at most m * d.

theorem MIPStarRE.LDT.Preliminaries.schwartzZippel_totalDegree {m d : ℕ} {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {g h : MvPolynomial (Fin m) K} (hneq : g ≠ h) (hg : g.totalDegree ≤ d) (hh : h.totalDegree ≤ d) : polynomialAgreementProbability m K g h ≤ ↑d / ↑(Fintype.card K)

If two polynomials on K^m have total degree at most d, then the uniform agreement probability is at most d / |K|.

theorem MIPStarRE.LDT.Preliminaries.schwartzZippel_individualDegree {m d : ℕ} {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (g h : ↥(polyFunc m K d)) (hneq : g ≠ h) : polynomialAgreementProbability m K ↑g ↑h ≤ ↑(m * d) / ↑(Fintype.card K)

Schwartz-Zippel for the paper's low-individual-degree class \polyfunc{m}{q}{d}.