Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Block.Recursion.Scheduled.Asymptotics.Defs

A fixed family of recursive extractors with polylogarithmic output #

For fixed natural parameters a,e, the leaf length is L=clog 2 (n+1) and the depth is exactly a*clog 2 (L+1). The local error exponent is e+h+2, and the reserve is the existing explicit finite reserve. These definitions instantiate the specified recursive map and its actual seeds. The depth is not truncated at small input lengths.

source
def Algebraic.Cutwidth.Extractor.polylogBlockLength (n : ℕ) :
ℕ

The number of output bits extracted from each leaf.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.polylogBlockDepth (a n : ℕ) :
    ℕ

    The raw recursion depth, with fixed multiplier a.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.polylogBlockErrorExponent (a e n : ℕ) :
      ℕ

      The local exponent paying for total error 2^(-e) at the chosen depth.

      Equations
      Instances For
        source
        def Algebraic.Cutwidth.Extractor.polylogBlockReserve (a e n : ℕ) :
        ℕ

        The explicit reserve used at every leaf of the family.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Algebraic.Cutwidth.Extractor.polylogBlockEntropy (a e n : ℕ) :
          ℕ

          The actual initial entropy in bits; the source cap is 2 raised to this number.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Algebraic.Cutwidth.Extractor.polylogBlockSeedBits (a e n : ℕ) :
            ℕ

            The exact total number of bits in all retained seeds.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Algebraic.Cutwidth.Extractor.polylogBlockOutputBits (a n : ℕ) :
              ℕ

              The actual number of Boolean output coordinates across all leaves.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                abbrev Algebraic.Cutwidth.Extractor.PolylogBlockSeeds (a e n : ℕ) :
                Type

                All field seeds retained by the specified member of the family.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def Algebraic.Cutwidth.Extractor.polylogBlockExtractor (a e n : ℕ) (x : Fin n → Bool) (seeds : PolylogBlockSeeds a e n) :
                  Fin (recursiveBlockCount 1 (polylogBlockDepth a n)) → Fin (polylogBlockLength n) → ZMod 2

                  The specified recursive extractor at length n, for fixed family parameters a,e.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For