Axis-line to global polynomial lifts

Utility lemmas for substituting a univariate axis-line polynomial into a chosen ambient coordinate.

theorem MIPStarRE.LDT.degreeOf_eval₂_C_X_le_natDegree {K : Type u_1} {σ : Type u_2} [Field K] [DecidableEq σ] (p : _root_.Polynomial K) (i j : σ) : MvPolynomial.degreeOf i (Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X j) p) ≤ if i = j then p.natDegree else 0

Substituting a univariate polynomial into one multivariate variable preserves its degree bound in that variable and gives degree zero in all other variables.

noncomputable def MIPStarRE.LDT.axisLinePolynomialToPolynomial (params : Parameters) [FieldModel params.q] (i : Fin params.m) (f : AxisLinePolynomial params) : Polynomial params

Extend an axis-line answer to a global polynomial by substituting the ambient coordinate X i for the formal line parameter. Away from direction i, the result is constant, so in the m = 1 base case this identifies the unique axis-parallel line polynomial with an ambient low-degree polynomial.

Equations

• MIPStarRE.LDT.axisLinePolynomialToPolynomial params i f = { poly := Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X i) f.poly, lowIndividualDegree := ⋯ }

@[simp]

theorem MIPStarRE.LDT.axisLinePolynomialToPolynomial_apply (params : Parameters) [FieldModel params.q] (i : Fin params.m) (f : AxisLinePolynomial params) (u : Point params) : (axisLinePolynomialToPolynomial params i f).toFun u = f.toFun (u i)

Evaluating the lifted polynomial at a point u recovers the original line polynomial at the ith coordinate u i.