Documentation

MIPRE.Background.LIDT.Adapter.Reparam

The seeded-CL adapter, part 2: affine reparametrization of a line answer #

Both tests answer a line question with a univariate polynomial in the parameter of the line, and they parametrize the same line differently: the base points differ by a multiple of the direction and the directions differ by a scalar (see MIPRE.Background.LIDT.Adapter.Geometry, and the correction in planning/lidt-cl-adapter.md). So converting an answer means substituting an affine map t ↦ a t + b into the polynomial — the "canonicalization and rebasing" of rem:lidt-cl-adapter.

Answers are coefficient vectors (LinePoly F k = Fin (k+1) → F), and the substitution has to preserve the degree bound exactly, since the bound is the answer alphabet: an adapter that raised the degree would not be producing an answer of the canonical-line test at all.

Doing this directly on coefficient vectors means a Taylor shift, hence the binomial theorem by hand. Going through Polynomial F avoids that entirely: toPoly and ofPoly are mutually inverse between coefficient vectors and polynomials of degree at most k (ofPoly_toPoly, toPoly_ofPoly), natDegree_comp_le gives the degree bound for free, and the inverse substitution is the composition with the inverse affine map, so the reparametrization is a bijection with no computation on coefficients at all.

Coefficient vectors and polynomials #

source
noncomputable def MIPRE.LIDT.Adapter.toPoly {F : Type u_1} [Field F] {k : ℕ} (f : LinePoly F k) :
Polynomial F

A coefficient vector, as a polynomial.

Equations
Instances For
    source
    def MIPRE.LIDT.Adapter.ofPoly {F : Type u_1} [Field F] {k : ℕ} (p : Polynomial F) :
    LinePoly F k

    A polynomial's coefficients, truncated to degree k.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LIDT.Adapter.ofPoly_apply {F : Type u_1} [Field F] {k : ℕ} (p : Polynomial F) (i : Fin (k + 1)) :
      ofPoly p i = p.coeff ↑i
      source
      theorem MIPRE.LIDT.Adapter.natDegree_toPoly_le {F : Type u_1} [Field F] {k : ℕ} (f : LinePoly F k) :
      (toPoly f).natDegree ≤ k
      source
      @[simp]
      theorem MIPRE.LIDT.Adapter.coeff_toPoly {F : Type u_1} [Field F] {k : ℕ} (f : LinePoly F k) (i : Fin (k + 1)) :
      (toPoly f).coeff ↑i = f i
      source
      @[simp]
      theorem MIPRE.LIDT.Adapter.ofPoly_toPoly {F : Type u_1} [Field F] {k : ℕ} (f : LinePoly F k) :
      ofPoly (toPoly f) = f
      source
      theorem MIPRE.LIDT.Adapter.eval_toPoly {F : Type u_1} [Field F] {k : ℕ} (f : LinePoly F k) (t : F) :
      Polynomial.eval t (toPoly f) = f.eval t

      Evaluation agrees with Polynomial.eval.

      source
      theorem MIPRE.LIDT.Adapter.toPoly_ofPoly {F : Type u_1} [Field F] {k : ℕ} {p : Polynomial F} (hp : p.natDegree ≤ k) :
      toPoly (ofPoly p) = p

      On polynomials of degree at most k, truncation loses nothing.

      source
      theorem MIPRE.LIDT.Adapter.eval_ofPoly {F : Type u_1} [Field F] {k : ℕ} {p : Polynomial F} (hp : p.natDegree ≤ k) (t : F) :
      (ofPoly p).eval t = Polynomial.eval t p

      Evaluating the truncation of a polynomial of degree at most k.

      The affine substitution #

      source
      noncomputable def MIPRE.LIDT.Adapter.affineMap {F : Type u_1} [Field F] (a b : F) :
      Polynomial F

      The affine map to substitute.

      Equations
      Instances For
        source
        theorem MIPRE.LIDT.Adapter.natDegree_affineMap_le {F : Type u_1} [Field F] (a b : F) :
        (affineMap a b).natDegree ≤ 1
        source
        @[simp]
        theorem MIPRE.LIDT.Adapter.eval_affineMap {F : Type u_1} [Field F] (a b t : F) :
        Polynomial.eval t (affineMap a b) = a * t + b
        source
        noncomputable def MIPRE.LIDT.Adapter.reparam {F : Type u_1} [Field F] {k : ℕ} (a b : F) (f : LinePoly F k) :
        LinePoly F k

        Affine reparametrization of an answer: reparam a b f is the coefficient vector of t ↦ f (a t + b), of the same degree bound.

        Equations
        Instances For
          source
          theorem MIPRE.LIDT.Adapter.natDegree_comp_affineMap_le {F : Type u_1} [Field F] {k : ℕ} (a b : F) (f : LinePoly F k) :
          ((toPoly f).comp (affineMap a b)).natDegree ≤ k
          source
          @[simp]
          theorem MIPRE.LIDT.Adapter.eval_reparam {F : Type u_1} [Field F] {k : ℕ} (a b : F) (f : LinePoly F k) (t : F) :
          (reparam a b f).eval t = f.eval (a * t + b)