Coefficient vectors of low-individual-degree polynomials

LowIndDegPoly F n d is a coefficient vector indexed by exponent vectors with entries at most d. This file is the algebra of those vectors that more than one analysis needs, moved here from the Pauli basis test's Dummy.lean and Linear.lean (where it was first written) so that the simultaneous low-degree test, which sits below the Pauli test in the import graph, can use it. The names are unchanged.

• Schwartz--Zippel for any finite variable type (prob_agreeOn_le_individualDegree), and the bridge LowIndDegPoly.toMv to MvPolynomial with its evaluation, coefficient and individual-degree facts; card_eval_eq_zero_le is the form a nonzero coefficient vector needs.
• Coefficients of a monomial pattern. LowIndDegPoly.coef g T t is the coefficient vector, in the variables outside T, of the monomial ∏_{k ∈ T} u_k^{t k}, and eval_eq_sum_coef is the decomposition g(u) = ∑_t u^t_T · (coef g T t)(u).

Schwartz--Zippel for any finite variable type

def MIPRE.LowDegree.agreeOn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {σ : Type u_2} [Fintype σ] [DecidableEq σ] (f g : MvPolynomial σ F) : Finset (σ → F)

The points of F^σ at which two polynomials agree.

Equations

• MIPRE.LowDegree.agreeOn f g = {x : σ → F | (MvPolynomial.eval x) f = (MvPolynomial.eval x) g}

@[simp]

theorem MIPRE.LowDegree.mem_agreeOn {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {f g : MvPolynomial σ F} {x : σ → F} : x ∈ agreeOn f g ↔ (MvPolynomial.eval x) f = (MvPolynomial.eval x) g

theorem MIPRE.LowDegree.prob_agreeOn_le_individualDegree {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {σ : Type u_2} [Fintype σ] [DecidableEq σ] {f g : MvPolynomial σ F} (hfg : f ≠ g) {d : ℕ} (hf : ∀ (i : σ), MvPolynomial.degreeOf i f ≤ d) (hg : ∀ (i : σ), MvPolynomial.degreeOf i g ≤ d) : ↑(agreeOn f g).card / ↑(Fintype.card F) ^ Fintype.card σ ≤ ↑(Fintype.card σ) * ↑d / ↑(Fintype.card F)

Schwartz--Zippel, individual-degree form, for any finite variable type: two unequal polynomials of individual degree at most d in the variables σ agree at a uniformly random point of F^σ with probability at most |σ| d / q.

Coefficient vectors as polynomials

noncomputable def MIPRE.LIDT.expFinsupp {n d : ℕ} (e : Fin n → Fin (d + 1)) : Fin n →₀ ℕ

An exponent vector with entries at most d, as a finitely supported function.

Equations

• MIPRE.LIDT.expFinsupp e = Finsupp.equivFunOnFinite.symm fun (i : Fin n) => ↑(e i)

@[simp]

theorem MIPRE.LIDT.expFinsupp_apply {n d : ℕ} (e : Fin n → Fin (d + 1)) (i : Fin n) : (expFinsupp e) i = ↑(e i)

theorem MIPRE.LIDT.expFinsupp_injective {n d : ℕ} : Function.Injective expFinsupp

noncomputable def MIPRE.LIDT.LowIndDegPoly.toMv {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) : MvPolynomial (Fin n) F

The polynomial a coefficient vector denotes.

Equations

• g.toMv = ∑ e : Fin n → Fin (d + 1), (MvPolynomial.monomial (MIPRE.LIDT.expFinsupp e)) (g e)

theorem MIPRE.LIDT.LowIndDegPoly.eval_toMv {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (u : Point F n) : (MvPolynomial.eval u) g.toMv = g.eval u

theorem MIPRE.LIDT.LowIndDegPoly.coeff_toMv {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (e : Fin n → Fin (d + 1)) : g.toMv.coeff (expFinsupp e) = g e

theorem MIPRE.LIDT.LowIndDegPoly.degreeOf_toMv_le {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (i : Fin n) : MvPolynomial.degreeOf i g.toMv ≤ d

theorem MIPRE.LIDT.degreeOf_rename_le {F : Type u_1} [Field F] {σ : Type u_2} {τ : Type u_3} {p : MvPolynomial σ F} {f : σ → τ} (hf : Function.Injective f) {d : ℕ} (hp : ∀ (i : σ), MvPolynomial.degreeOf i p ≤ d) (j : τ) : MvPolynomial.degreeOf j ((MvPolynomial.rename f) p) ≤ d

Renaming along an injection keeps individual degrees bounded, at every target variable.

Coefficients of a monomial pattern

theorem MIPRE.LIDT.LowIndDegPoly.eval_sub {F : Type u_1} [Field F] {n d : ℕ} (p q : LowIndDegPoly) (u : Point F n) : (p - q).eval u = p.eval u - q.eval u

Evaluation of coefficient vectors is additive: (p - q)(u) = p(u) - q(u).

def MIPRE.LIDT.patch {n d : ℕ} (T : Finset (Fin n)) (t e : Fin n → Fin (d + 1)) : Fin n → Fin (d + 1)

The exponent vector e with its coordinates in T replaced by those of the pattern t.

Equations

• MIPRE.LIDT.patch T t e k = if k ∈ T then t k else e k

def MIPRE.LIDT.maskOn {n d : ℕ} (T : Finset (Fin n)) (e : Fin n → Fin (d + 1)) : Fin n → Fin (d + 1)

The part of an exponent vector on T.

Equations

• MIPRE.LIDT.maskOn T e k = if k ∈ T then e k else 0

def MIPRE.LIDT.maskOff {n d : ℕ} (T : Finset (Fin n)) (e : Fin n → Fin (d + 1)) : Fin n → Fin (d + 1)

The part of an exponent vector off T.

Equations

• MIPRE.LIDT.maskOff T e k = if k ∈ T then 0 else e k

theorem MIPRE.LIDT.patch_maskOn_maskOff {n d : ℕ} (T : Finset (Fin n)) (e : Fin n → Fin (d + 1)) : patch T (maskOn T e) (maskOff T e) = e

theorem MIPRE.LIDT.maskOn_patch {n d : ℕ} (T : Finset (Fin n)) (t e : Fin n → Fin (d + 1)) : maskOn T (patch T t e) = maskOn T t

theorem MIPRE.LIDT.maskOff_patch {n d : ℕ} (T : Finset (Fin n)) (t e : Fin n → Fin (d + 1)) : maskOff T (patch T t e) = maskOff T e

theorem MIPRE.LIDT.maskOn_eq_self {n d : ℕ} {T : Finset (Fin n)} {t : Fin n → Fin (d + 1)} (h : ∀ k ∉ T, t k = 0) : maskOn T t = t

theorem MIPRE.LIDT.maskOff_eq_self {n d : ℕ} {T : Finset (Fin n)} {e : Fin n → Fin (d + 1)} (h : ∀ k ∈ T, e k = 0) : maskOff T e = e

theorem MIPRE.LIDT.maskOn_apply_of_not {n d : ℕ} {T : Finset (Fin n)} (e : Fin n → Fin (d + 1)) {k : Fin n} (hk : k ∉ T) : maskOn T e k = 0

theorem MIPRE.LIDT.maskOff_apply_of {n d : ℕ} {T : Finset (Fin n)} (e : Fin n → Fin (d + 1)) {k : Fin n} (hk : k ∈ T) : maskOff T e k = 0

def MIPRE.LIDT.LowIndDegPoly.coef {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (T : Finset (Fin n)) (t : Fin n → Fin (d + 1)) : LowIndDegPoly

The coefficient of a monomial pattern: the coefficient vector, in the variables outside T, of the monomial ∏_{k ∈ T} u_k^{t k} in g; zero unless the pattern is supported in T.

Equations

• g.coef T t e = if (∀ k ∈ T, e k = 0) ∧ ∀ k ∉ T, t k = 0 then g (MIPRE.LIDT.patch T t e) else 0

theorem MIPRE.LIDT.prod_pow_patch {F : Type u_1} [Field F] {n d : ℕ} (T : Finset (Fin n)) (u : Point F n) {t e : Fin n → Fin (d + 1)} (he : ∀ k ∈ T, e k = 0) : (∏ k ∈ T, u k ^ ↑(t k)) * ∏ k : Fin n, u k ^ ↑(e k) = ∏ k : Fin n, u k ^ ↑(patch T t e k)

The product of powers splits along T.

theorem MIPRE.LIDT.LowIndDegPoly.eval_eq_sum_coef {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (T : Finset (Fin n)) (u : Point F n) : g.eval u = ∑ t : Fin n → Fin (d + 1), (∏ k ∈ T, u k ^ ↑(t k)) * (g.coef T t).eval u

Decomposition along the patterns on T: g(u) = ∑_t u^t_T · (coef g T t)(u).

theorem MIPRE.LIDT.LowIndDegPoly.eval_coef_of_eq_off {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (T : Finset (Fin n)) (t : Fin n → Fin (d + 1)) {u u' : Point F n} (h : ∀ k ∉ T, u k = u' k) : (g.coef T t).eval u = (g.coef T t).eval u'

A coefficient vector on T reads no coordinate in T.

theorem MIPRE.LIDT.LowIndDegPoly.coef_maskOff {F : Type u_1} [Field F] {n d : ℕ} (g : LowIndDegPoly) (T : Finset (Fin n)) (e : Fin n → Fin (d + 1)) : g.coef T (maskOn T e) (maskOff T e) = g e

A coefficient vector is nonzero where the polynomial has a nonzero coefficient with the pattern.

theorem MIPRE.LIDT.card_eval_eq_zero_le {F : Type u_1} [Field F] {n d : ℕ} [Fintype F] [DecidableEq F] {G : LowIndDegPoly} (hG : G ≠ 0) : ↑{u : Point F n | G.eval u = 0}.card / ↑(Fintype.card F) ^ n ≤ ↑n * ↑d / ↑(Fintype.card F)

Schwartz--Zippel for a nonzero coefficient vector: it vanishes at a uniform point with probability at most n d / q.