Bridge, part 2: polynomial answer alphabets

Our answer alphabets are coefficient vectors (LinePoly F n := Fin (n+1) → F) and coefficient tables (LowIndDegPoly := (Fin m → Fin (d+1)) → F); the MIPStarRE development uses subtypes of Mathlib's Polynomial and MvPolynomial with degree bounds (AxisLinePolynomial, DiagonalLinePolynomial, MIPStarRE.LDT.Polynomial). This file provides the equivalences between the two, and shows that evaluation is compatible with them through the field coding.

Univariate polynomials from coefficient vectors

noncomputable def MIPRE.LIDT.Bridge.ofCoeffs {F : Type u_1} [Field F] {n : ℕ} (c : LinePoly F n) : Polynomial F

The univariate polynomial with the given coefficients.

Equations

• MIPRE.LIDT.Bridge.ofCoeffs c = ∑ i : Fin (n + 1), Polynomial.C (c i) * Polynomial.X ^ ↑i

theorem MIPRE.LIDT.Bridge.natDegree_ofCoeffs_le {F : Type u_1} [Field F] {n : ℕ} (c : LinePoly F n) : (ofCoeffs c).natDegree ≤ n

theorem MIPRE.LIDT.Bridge.coeff_ofCoeffs {F : Type u_1} [Field F] {n : ℕ} (c : LinePoly F n) (i : Fin (n + 1)) : (ofCoeffs c).coeff ↑i = c i

theorem MIPRE.LIDT.Bridge.ofCoeffs_coeff {F : Type u_1} [Field F] {n : ℕ} (p : Polynomial F) (hp : p.natDegree ≤ n) : (ofCoeffs fun (i : Fin (n + 1)) => p.coeff ↑i) = p

theorem MIPRE.LIDT.Bridge.eval_ofCoeffs {F : Type u_1} [Field F] {n : ℕ} (c : LinePoly F n) (t : F) : Polynomial.eval t (ofCoeffs c) = c.eval t

noncomputable def MIPRE.LIDT.Bridge.axisEquiv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : LinePoly F d ≃ MIPStarRE.LDT.AxisLinePolynomial (lidtParams F m d)

Axis-line answers: coefficient vectors of length d + 1 versus polynomials of degree at most d.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.LIDT.Bridge.diagEquiv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : LinePoly F (m * d) ≃ MIPStarRE.LDT.DiagonalLinePolynomial (lidtParams F m d)

Diagonal-line answers: coefficient vectors of length m·d + 1 versus polynomials of degree at most m·d.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LIDT.Bridge.axisEquiv_poly {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LinePoly F d) : (axisEquiv c).poly = ofCoeffs c

@[simp]

theorem MIPRE.LIDT.Bridge.diagEquiv_poly {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LinePoly F (m * d)) : (diagEquiv c).poly = ofCoeffs c

theorem MIPRE.LIDT.Bridge.axisEquiv_apply_enc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LinePoly F d) (t : F) : (axisEquiv c).toFun (enc t) = enc (c.eval t)

Evaluating an axis-line answer at a coded parameter.

theorem MIPRE.LIDT.Bridge.diagEquiv_apply_enc {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LinePoly F (m * d)) (t : F) : (diagEquiv c).toFun (enc t) = enc (c.eval t)

Evaluating a diagonal-line answer at a coded parameter.

Multivariate polynomials from coefficient tables

noncomputable def MIPRE.LIDT.Bridge.expo {m d : ℕ} (e : Fin m → Fin (d + 1)) : Fin m →₀ ℕ

The exponent vector of a monomial index.

Equations

• MIPRE.LIDT.Bridge.expo e = Finsupp.equivFunOnFinite.symm fun (i : Fin m) => ↑(e i)

@[simp]

theorem MIPRE.LIDT.Bridge.expo_apply {m d : ℕ} (e : Fin m → Fin (d + 1)) (i : Fin m) : (expo e) i = ↑(e i)

theorem MIPRE.LIDT.Bridge.expo_injective {m d : ℕ} : Function.Injective expo

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

The multivariate polynomial with the given coefficient table.

Equations

• MIPRE.LIDT.Bridge.toMv c = ∑ e : Fin m → Fin (d + 1), (MvPolynomial.monomial (MIPRE.LIDT.Bridge.expo e)) (c e)

theorem MIPRE.LIDT.Bridge.coeff_toMv {F : Type u_1} [Field F] {m d : ℕ} (c : LowIndDegPoly) (e : Fin m → Fin (d + 1)) : MvPolynomial.coeff (expo e) (toMv c) = c e

theorem MIPRE.LIDT.Bridge.coeff_toMv_of_not_le {F : Type u_1} [Field F] {m d : ℕ} (c : LowIndDegPoly) (s : Fin m →₀ ℕ) (hs : ¬∀ (i : Fin m), s i ≤ d) : MvPolynomial.coeff s (toMv c) = 0

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

theorem MIPRE.LIDT.Bridge.toMv_coeff {F : Type u_1} [Field F] {m d : ℕ} (p : MvPolynomial (Fin m) F) (hp : ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d) : (toMv fun (e : Fin m → Fin (d + 1)) => MvPolynomial.coeff (expo e) p) = p

A polynomial of bounded individual degree is determined by its coefficient table.

theorem MIPRE.LIDT.Bridge.polynomial_ext {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] {g g' : MIPStarRE.LDT.Polynomial (lidtParams F m d)} (h : g.poly = g'.poly) : g = g'

Extensionality for MIPStarRE's global polynomial answers.

noncomputable def MIPRE.LIDT.Bridge.lowIndDegEquiv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] : LowIndDegPoly ≃ MIPStarRE.LDT.Polynomial (lidtParams F m d)

Global answers: coefficient tables versus polynomials of individual degree at most d.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.LIDT.Bridge.lowIndDegEquiv_poly {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LowIndDegPoly) : (lowIndDegEquiv c).poly = toMv c

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

theorem MIPRE.LIDT.Bridge.lowIndDegEquiv_apply_encP {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (c : LowIndDegPoly) (u : Point F m) : (lowIndDegEquiv c).toFun (encP u) = enc (c.eval u)

Evaluating a global answer at a coded point.