Finite answer spaces for the low individual degree test

Finite-type instances for the bounded polynomial answer spaces defined in MIPStarRE.LDT.Basic.LowDegreePolynomial.

Finite answer spaces

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.instDecidableEqAxisLinePolynomial (params : Parameters) [FieldModel params.q] : DecidableEq (AxisLinePolynomial params)

The axis-line polynomial answer type uses classical equality on the bundled polynomial witness.

Equations

• MIPStarRE.LDT.instDecidableEqAxisLinePolynomial params = Classical.decEq (MIPStarRE.LDT.AxisLinePolynomial params)

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.instDecidableEqPolynomial (params : Parameters) [FieldModel params.q] : DecidableEq (Polynomial params)

The finite low-individual-degree polynomial answer type uses classical equality on the bundled polynomial witness.

Equations

• MIPStarRE.LDT.instDecidableEqPolynomial params = Classical.decEq (MIPStarRE.LDT.Polynomial params)

theorem MIPStarRE.LDT.linePolynomial_coeff_fin_injective (params : Parameters) [FieldModel params.q] {n : ℕ} {p q : LinePolynomialModel params} (hp : Polynomial.natDegree p ≤ n) (hq : Polynomial.natDegree q ≤ n) (h : ∀ (i : Fin (n + 1)), Polynomial.coeff p ↑i = Polynomial.coeff q ↑i) : p = q

A univariate polynomial of natDegree ≤ n is determined by its first n + 1 coefficients. Shared injectivity fact behind the finite-answer-space instances below.

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.instFintypeAxisLinePolynomial (params : Parameters) [FieldModel params.q] : Fintype (AxisLinePolynomial params)

Axis-line polynomial answers form a finite type via their bounded coefficient vectors.

Equations

• MIPStarRE.LDT.instFintypeAxisLinePolynomial params = Fintype.ofInjective (fun (f : MIPStarRE.LDT.AxisLinePolynomial params) (i : Fin (params.d + 1)) => Polynomial.coeff f.poly ↑i) ⋯

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.instFintypeDiagonalLinePolynomial (params : Parameters) [FieldModel params.q] : Fintype (DiagonalLinePolynomial params)

Diagonal-line polynomial answers form a finite type via their bounded coefficient vectors.

Equations

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

@[instance_reducible]

noncomputable instance MIPStarRE.LDT.instFintypePolynomial (params : Parameters) [FieldModel params.q] : Fintype (Polynomial params)

Global low-individual-degree polynomial answers form a finite type, by injecting into the finite space of degree-restricted multivariate polynomials.

Equations

• MIPStarRE.LDT.instFintypePolynomial params = Fintype.ofInjective (fun (g : MIPStarRE.LDT.Polynomial params) => ⟨g.poly, ⋯⟩) ⋯

theorem MIPStarRE.LDT.polynomial_sum_fiberwise (params : Parameters) [FieldModel params.q] (u : Point params) {β : Type u_1} [AddCommMonoid β] (f : Polynomial params → β) : ∑ h : Polynomial params, f h = ∑ a : Fq params, ∑ h : Polynomial params with h.toFun u = a, f h

Reindex a polynomial-indexed sum by the value of the polynomial at a fixed point.

The low individual degree test frequently groups global polynomial answers by the fiber of the evaluation map h ↦ h u. This lemma records that finite reindexing in the notation used throughout the LDT formalization.