Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Condenser.Parameters.Explicit.Defs

Explicit finite parameters for the binary condenser #

The slack budget pays for error 2^(-e) and a linear bound on the extension degree. The sparse field choice determines the base coefficient width, after which the extension degree is rounded to a power of three large enough to hold n source bits. The minimum extension degree is three.

source
def Algebraic.Cutwidth.Extractor.explicitCondenserBudget (n k e : ℕ) :
ℕ

Slack bits for source length, entropy, and inverse error.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.explicitCondenserExtensionExponent (n k e u : ℕ) :
    ℕ

    Select an extension degree that covers the source and is at least three.

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

      The selected extension degree is a power of three.

      Equations
      Instances For