Restricting a polynomial to a line

The expansion stage's line measurements are indexed by the restriction to a line of the low-degree encoding of the ancilla's measurement outcome. This file is that operation: substitute the affine parametrization t -> u0 + t . w into a multivariate polynomial and read off the univariate coefficients.

Two facts are all the consumers need:

• eval_lineRestrict --- evaluating the restriction at t is evaluating the polynomial at the point u0 + t . w, so the restriction carries the same information along the line;
• natDegree_lineRestrict_le --- the restriction has degree at most the total degree, so a multilinear polynomial in m variables restricts to degree at most m and the coefficient vector fits in a LinePoly F m.

lineCoeffs packages the coefficients as the LinePoly the games use, and eval_lineCoeffs is the composite of the two.

noncomputable def MIPRE.LowDegree.lineRestrict {F : Type u_1} [Field F] {m : ℕ} (u₀ w : Fin m → F) (p : MvPolynomial (Fin m) F) : Polynomial F

The restriction of a multivariate polynomial to the line t ↦ u₀ + t • w, as a univariate polynomial.

Equations

• MIPRE.LowDegree.lineRestrict u₀ w p = (MvPolynomial.aeval fun (i : Fin m) => Polynomial.C (u₀ i) + Polynomial.X * Polynomial.C (w i)) p

@[simp]

theorem MIPRE.LowDegree.lineRestrict_zero {F : Type u_1} [Field F] {m : ℕ} (u₀ w : Fin m → F) : lineRestrict u₀ w 0 = 0

theorem MIPRE.LowDegree.eval_lineRestrict {F : Type u_1} [Field F] {m : ℕ} (u₀ w : Fin m → F) (p : MvPolynomial (Fin m) F) (t : F) : Polynomial.eval t (lineRestrict u₀ w p) = (MvPolynomial.eval (u₀ + t • w)) p

Evaluating the restriction is evaluating along the line.

theorem MIPRE.LowDegree.natDegree_lineRestrict_le {F : Type u_1} [Field F] {m : ℕ} (u₀ w : Fin m → F) (p : MvPolynomial (Fin m) F) : (lineRestrict u₀ w p).natDegree ≤ p.totalDegree

The restriction has degree at most the total degree.

theorem MIPRE.LowDegree.natDegree_lineRestrict_single_le {F : Type u_1} [Field F] {m : ℕ} (u₀ : Fin m → F) (j : Fin m) (p : MvPolynomial (Fin m) F) : (lineRestrict u₀ (Pi.single j 1) p).natDegree ≤ MvPolynomial.degreeOf j p

On an axis-parallel line the restriction has degree at most the individual degree in that coordinate. Along u_0 + t e_j only the j-th variable moves, so every other substitution is a constant and the degree in t is the degree of p in X_j. This is what makes a multilinear encoding restrict to an affine function of the line parameter.

theorem MIPRE.LowDegree.sum_coeff_lineRestrict {F : Type u_1} [Field F] {m n : ℕ} {p : MvPolynomial (Fin m) F} (hp : p.totalDegree ≤ n) (u₀ w : Fin m → F) (t : F) : ∑ i : Fin (n + 1), (lineRestrict u₀ w p).coeff ↑i * t ^ ↑i = (MvPolynomial.eval (u₀ + t • w)) p

The coefficient vector of the restriction, evaluated at t. This is the form the games use: a polynomial of degree at most n is a vector of n + 1 coefficients, and evaluating that vector at t is evaluating the polynomial along the line.