Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Strong.Block.Splitting.Iterated.Defs

Splitting successive pairs of blocks #

Each pair keeps its two coordinates next to each other: pair i occupies positions 2*i and 2*i+1. The tuple equivalence and the two-coordinate prepend equivalence also cover empty tails and empty alphabets.

This is the coordinate map in Chattopadhyay--Goodman--Liao, Corollary 5.4 of Affine Extractors for Almost Logarithmic Entropy: https://eccc.weizmann.ac.il/report/2021/075/download/.

source
def Algebraic.Cutwidth.Extractor.splitBlockIndexEquiv (t : ℕ) :
Fin t × Fin 2 ≃ Fin (2 * t)

Pair number i and within-pair coordinate j occupy position j + 2*i.

Equations
Instances For
    source
    def Algebraic.Cutwidth.Extractor.splitBlockEquiv (α : Type u_1) (t : ℕ) :
    (Fin t → α × α) ≃ (Fin (2 * t) → α)

    Flatten pairs in their original order, retaining both coordinates of each pair.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Algebraic.Cutwidth.Extractor.pairPrependEquiv (α : Type u_1) (t : ℕ) :
      (α × α) × (Fin t → α) ≃ (Fin (t + 2) → α)

      Prepend the two coordinates of a pair to a tail tuple.

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