Documentation

MIPRE.Foundations.LowDegree.BinarySubstitution

Polynomial-time substitution of a unary-specified positive power #

source
def MIPRE.LowDegree.BinaryPolynomial.substitutePowerBits (a : Cost.BitStr) (u : Cost.Unary) :
Cost.BitStr

Substitute X^(u.length+1) by inserting the requested number of zero coefficients. The exponent is positive by construction; an empty unary parameter means substitution by X.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_substitutePowerBits {R : Type u_1} [CommRing R] (z : R) (a : Cost.BitStr) (u : Cost.Unary) :
    evalBits z (substitutePowerBits a u) = evalBits (z ^ (List.length u + 1)) a

    Substitution has the expected Horner semantics in every commutative ring.

    source
    theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_substitutePowerBits (a : Cost.BitStr) (u : Cost.Unary) :
    polyOfBits (substitutePowerBits a u) = (polyOfBits a).comp (Polynomial.X ^ (List.length u + 1))

    The executable substitution agrees with Mathlib polynomial composition.

    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.coefficientBlockProg :
    Cost.PolyTimeFun (Bool × Cost.Unary) Cost.BitStr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.flattenCoefficientsProg :
      Cost.PolyTimeFun (List Cost.BitStr) Cost.BitStr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.substitutePowerBitsProg :
        Cost.PolyTimeFun (Cost.BitStr × Cost.Unary) Cost.BitStr

        A fixed ambient program for positive-power substitution on arbitrary coefficient lists.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.substitutePowerBitsProg_apply (a : Cost.BitStr) (u : Cost.Unary) :
          substitutePowerBitsProg.toFun (a, u) = substitutePowerBits a u