Documentation

MIPRE.Foundations.LowDegree.BinaryNormalize

Normalizing binary coefficient lists #

Remove trailing false coefficients by a right fold. The empty list represents zero; every nonzero result ends in true. Both semantics and the ambient bound hold on arbitrary coefficient lists, including redundant trailing zeros.

source
def MIPRE.LowDegree.BinaryPolynomial.normalizeStep (a : Cost.BitStr) (b : Bool) :
Cost.BitStr

Prepend a coefficient, suppressing zero coefficients above the leading term.

Equations
Instances For
    source
    def MIPRE.LowDegree.BinaryPolynomial.normalizeBits (a : Cost.BitStr) :
    Cost.BitStr

    Canonical coefficient list, with no trailing false coefficients.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.normalizeBits_nil :
      normalizeBits [] = []
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.normalizeBits_cons (b : Bool) (a : Cost.BitStr) :
      normalizeBits (b :: a) = normalizeStep (normalizeBits a) b
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.length_normalizeStep_le (a : Cost.BitStr) (b : Bool) :
      List.length (normalizeStep a b) ≤ List.length a + 1

      Normalizing cannot increase the coefficient width.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.length_normalizeBits_le (a : Cost.BitStr) :
      List.length (normalizeBits a) ≤ List.length a

      The normalized representation is no longer than its input.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_normalizeStep {R : Type u_1} [CommRing R] (z : R) (a : Cost.BitStr) (b : Bool) :
      evalBits z (normalizeStep a b) = ofBool b + z * evalBits z a

      Suppression of high zero coefficients preserves evaluation in every ring.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.evalBits_normalizeBits {R : Type u_1} [CommRing R] (z : R) (a : Cost.BitStr) :
      evalBits z (normalizeBits a) = evalBits z a

      Normalization preserves Horner evaluation.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_eq_evalBits (a : Cost.BitStr) :
      polyOfBits a = evalBits Polynomial.X a

      The polynomial interpretation is Horner evaluation at the indeterminate.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_normalizeBits (a : Cost.BitStr) :
      polyOfBits (normalizeBits a) = polyOfBits a

      Normalization preserves the polynomial itself.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.normalizeBits_getLast (a : Cost.BitStr) :
      normalizeBits a = [] ∨ List.getLastD (normalizeBits a) false = true

      A nonempty normalized list has a leading coefficient equal to one.

      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.normalizeStepProg :
      Cost.PolyTimeFun (Cost.BitStr × Bool) Cost.BitStr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.LowDegree.BinaryPolynomial.normalizeStep_esize (a : Cost.BitStr) (b : Bool) :
        Cost.esize (normalizeStep a b) ≤ Cost.esize a + Cost.esize b + 1
        source
        theorem MIPRE.LowDegree.BinaryPolynomial.fold_normalizeStep_esize (l a : Cost.BitStr) :
        Cost.esize (List.foldl normalizeStep a l) ≤ Cost.esize a + Cost.esize l
        source
        theorem MIPRE.LowDegree.BinaryPolynomial.normalizeStep_bounded :
        normalizeStepProg.FoldBounded Polynomial.X
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.normalizeBitsProg :
        Cost.PolyTimeFun Cost.BitStr Cost.BitStr

        One fixed ambient program for canonical polynomial coefficient lists.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.normalizeBitsProg_apply (a : Cost.BitStr) :
          normalizeBitsProg.toFun a = normalizeBits a