Documentation

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

Finite recursive block condensation and splitting #

The initial map may already depend on an earlier seed. Each further level adds one fresh seed, uses it on every current block, and splits the resulting pairs in order. The seed type retains the earlier seed and every fresh seed exactly once. Alphabets and fresh-seed types may vary between levels.

These are deterministic finite maps and an explicit error sum. They model the recursion in Chattopadhyay--Goodman--Liao, Theorem 5.6 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. An encoded uniform evaluator and a concrete parameter schedule are separate.

source
def Algebraic.Cutwidth.Extractor.RecursiveSeeds (Earlier : Type u) (Fresh : ℕ → Type u) :
ℕ → Type u

Retain the initial seed and one fresh seed for every completed level.

Equations
Instances For
    source
    @[instance_reducible]
    instance Algebraic.Cutwidth.Extractor.instFintypeRecursiveSeeds (Earlier : Type u) (Fresh : ℕ → Type u) [Fintype Earlier] [(i : ℕ) → Fintype (Fresh i)] (n : ℕ) :
    Fintype (RecursiveSeeds Earlier Fresh n)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance Algebraic.Cutwidth.Extractor.instNonemptyRecursiveSeeds (Earlier : Type u) (Fresh : ℕ → Type u) [Nonempty Earlier] [∀ (i : ℕ), Nonempty (Fresh i)] (n : ℕ) :
    Nonempty (RecursiveSeeds Earlier Fresh n)
    source
    def Algebraic.Cutwidth.Extractor.recursiveBlockCount (t : ℕ) :
    ℕ → ℕ

    Every level splits each current block into two successive blocks.

    Equations
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.recursiveBlockMap {X : Type v} {Earlier : Type u} {Fresh : ℕ → Type u} {α : ℕ → Type w} {t : ℕ} (initial : X → Earlier → Fin t → α 0) (C : (i : ℕ) → α i → Fresh i → α (i + 1) × α (i + 1)) (n : ℕ) :
      X → RecursiveSeeds Earlier Fresh n → Fin (recursiveBlockCount t n) → α n

      Run the initial map, then one shared-seed condenser and split per level.

      Equations
      Instances For
        source
        noncomputable def Algebraic.Cutwidth.Extractor.recursiveBlockError (t : ℕ) (ε : ℕ → ℝ) (e : ℕ → ℕ) (n : ℕ) :
        ℝ

        Sum the condenser and splitting errors over all blocks entering each level.

        Equations
        Instances For