Documentation

MIPRE.Foundations.Introspection.PauliRowsProg

Packing the Pauli register into consecutive field rows #

source
noncomputable def MIPRE.Introspection.PauliStageProgram.packRows :
Cost.PolyTimeFun Fields (List Cost.BitStr)
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem MIPRE.Introspection.PauliStageProgram.packRows_apply (x z : List Cost.BitStr) (s : Cost.BitStr) (v : List Cost.BitStr) (rx rz : Cost.BitStr) :
    packRows.toFun (x, z, s, v, rx, rz) = x ++ (z ++ s :: (v ++ [rx, rz]))
    source
    noncomputable def MIPRE.Introspection.PauliStageProgram.unpackRows :
    Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) Fields
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.PauliStageProgram.unpackRows_packRows (m : ℕ) (x z : List Cost.BitStr) (s : Cost.BitStr) (v : List Cost.BitStr) (rx rz : Cost.BitStr) (hx : x.length = m) (hz : z.length = m) (hv : v.length = m) :
      unpackRows.toFun (Cost.unary m, packRows.toFun (x, z, s, v, rx, rz)) = (x, z, s, v, rx, rz)
      source
      @[reducible, inline]
      abbrev MIPRE.Introspection.PauliStageProgram.RowInput :
      Type

      Input to a row query: widths, type, stage, prefix rows, vector rows.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def MIPRE.Introspection.PauliStageProgram.rowInput :
        Cost.PolyTimeFun RowInput Input
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.Introspection.PauliStageProgram.linearRows :
          Cost.PolyTimeFun RowInput (List Cost.BitStr)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MIPRE.Introspection.PauliStageProgram.marginalRows :
            Cost.PolyTimeFun RowInput (List Cost.BitStr)
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[reducible, inline]
              abbrev MIPRE.Introspection.PauliStageProgram.BinaryInput :
              Type

              Binary queries convert basis coordinates on entry and exit.

              Equations
              Instances For
                source
                noncomputable def MIPRE.Introspection.PauliStageProgram.binaryInput :
                Cost.PolyTimeFun BinaryInput RowInput
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MIPRE.Introspection.PauliStageProgram.linearBits :
                  Cost.PolyTimeFun BinaryInput Cost.BitStr
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def MIPRE.Introspection.PauliStageProgram.marginalBits :
                    Cost.PolyTimeFun BinaryInput Cost.BitStr
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For