Documentation

MIPRE.Foundations.LowDegree.BinaryCirculantProg

Executable circulant matrices and their inverse square roots #

source
def MIPRE.LowDegree.BinaryLinear.rotateLeftBits :
Cost.BitStr → Cost.BitStr
Equations
Instances For
    source
    theorem MIPRE.LowDegree.BinaryLinear.rotateLeftBits_eq_rotate (l : Cost.BitStr) :
    rotateLeftBits l = List.rotate l 1
    source
    def MIPRE.LowDegree.BinaryLinear.rotateRightBits (l : Cost.BitStr) :
    Cost.BitStr
    Equations
    Instances For
      source
      theorem MIPRE.LowDegree.BinaryLinear.esize_rotateLeftBits (l : Cost.BitStr) :
      Cost.esize (rotateLeftBits l) = Cost.esize l
      source
      theorem MIPRE.LowDegree.BinaryLinear.esize_rotateRightBits (l : Cost.BitStr) :
      Cost.esize (rotateRightBits l) = Cost.esize l
      source
      noncomputable def MIPRE.LowDegree.BinaryLinear.rotateLeftBitsProg :
      Cost.PolyTimeFun Cost.BitStr Cost.BitStr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryLinear.rotateRightBitsProg :
        Cost.PolyTimeFun Cost.BitStr Cost.BitStr
        Equations
        Instances For
          source
          theorem MIPRE.LowDegree.BinaryLinear.iterate_rotateRightBits (n : ℕ) (l : Cost.BitStr) :
          rotateRightBits^[n] l = ((List.reverse l).rotate n).reverse
          source
          theorem MIPRE.LowDegree.BinaryLinear.rotateRightBitsProg_iterate_size (n : ℕ) (l : Cost.BitStr) :
          Cost.esize (rotateRightBitsProg.toFun^[n] l) ≤ Polynomial.eval (Cost.esize l) Polynomial.X
          source
          theorem MIPRE.LowDegree.BinaryLinear.reverse_vectorBits {k : ℕ} (v : Fin k → ZMod 2) :
          List.reverse (vectorBits v) = vectorBits fun (i : Fin k) => v i.rev
          source
          theorem MIPRE.LowDegree.BinaryLinear.rotate_vectorBits {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) (j : Fin k) :
          List.rotate (vectorBits v) ↑j = vectorBits fun (i : Fin k) => v (i + j)
          source
          theorem MIPRE.LowDegree.BinaryLinear.iterate_rotateRightBits_vectorBits {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) (j : Fin k) :
          rotateRightBits^[↑j] (vectorBits v) = vectorBits fun (i : Fin k) => v (i - j)

          Right rotation is translation by the negative column index.

          source
          noncomputable def MIPRE.LowDegree.BinaryLinear.circulantBitsProg :
          Cost.PolyTimeFun Cost.BitStr (List Cost.BitStr)

          Print a circulant from its first column. The size and all iteration counts come from the input.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.LowDegree.BinaryLinear.circulantBitsProg_correct {k : ℕ} [NeZero k] (v : Fin k → ZMod 2) :
            circulantBitsProg.toFun (vectorBits v) = matrixBits (Matrix.circulant v)
            source
            theorem MIPRE.LowDegree.BinaryLinear.rootBitsProg_vectorBits {k : ℕ} [NeZero k] (hk : Odd k) (v : Fin k → ZMod 2) :
            rootBitsProg.toFun (vectorBits v) = vectorBits fun (i : Fin k) => v (i + i)

            The coefficient square-root program uses doubled indices also for Fin k coordinates.

            source
            noncomputable def MIPRE.LowDegree.BinaryLinear.inverseRootMatrixProg :
            Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

            Compute the inverse matrix, read its first column, permute doubled indices, then print the circulant square root.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MIPRE.LowDegree.BinaryLinear.inverseRootMatrixProg_correct {k : ℕ} [NeZero k] (hk : Odd k) (A : Matrix (Fin k) (Fin k) (ZMod 2)) :
              inverseRootMatrixProg.toFun (Cost.unary k, matrixBits A) = matrixBits (inverseRootMatrix A)