The auxiliary-unary distribution -- definitions

For a positive size parameter m, Hirahara's auxiliary-unary distribution chooses a clock length t uniformly from {1, ..., m}, chooses a uniform binary string x of length m - t, and outputs the canonical encoding of (x, 1^t).

We represent the same experiment by choosing the binary length n = m - t uniformly from {0, ..., m - 1} and an independent uniform m-bit string, whose first n bits are retained. The unused suffix makes all split choices live in one uniform finite seed space. At m = 0, where the paper's positive-length distribution is not specified, the totalized ensemble uses the unique empty seed and outputs pair [] []. Here m is the sum of the two component lengths; the self-delimiting binary encoding pair x 1^t has its own codec overhead and need not itself have list length m.

@[reducible, inline]

abbrev Complexity.AuxiliaryUnarySeed (m : ℕ) : Type

Uniform seed for the mth auxiliary-unary slice. The first component is the retained binary length; the second supplies both the retained prefix and ignored random suffix.

Equations

• Complexity.AuxiliaryUnarySeed m = (Fin (Nat.max 1 m) × (Fin m → Bool))

def Complexity.AuxiliaryUnarySeed.split {m : ℕ} (seed : AuxiliaryUnarySeed m) : ℕ

Length of the binary component selected by a seed.

Equations

• seed.split = ↑seed.1

theorem Complexity.AuxiliaryUnarySeed.splitLe {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.split ≤ m

Every selected binary length is at most the slice parameter, including the totalized zero slice.

def Complexity.AuxiliaryUnarySeed.bitBlocks {m n : ℕ} (hn : n ≤ m) : (Fin m → Bool) ≃ (Fin n → Bool) × (Fin (m - n) → Bool)

Split an m-bit string into a prefix of length n and the remaining suffix, for any certified n ≤ m.

Equations

• Complexity.AuxiliaryUnarySeed.bitBlocks hn = ((finCongr ⋯).arrowCongr (Equiv.refl Bool)).trans (Complexity.blockEquiv n (m - n))

def Complexity.AuxiliaryUnarySeed.binaryBits {m : ℕ} (seed : AuxiliaryUnarySeed m) : Fin seed.split → Bool

Retained random prefix selected by a seed.

Equations

• seed.binaryBits = ((Complexity.AuxiliaryUnarySeed.bitBlocks ⋯) seed.2).1

def Complexity.AuxiliaryUnarySeed.binary {m : ℕ} (seed : AuxiliaryUnarySeed m) : List Bool

Retained binary component as a list in increasing index order.

Equations

• seed.binary = List.ofFn seed.binaryBits

def Complexity.AuxiliaryUnarySeed.unary {m : ℕ} (seed : AuxiliaryUnarySeed m) : List Bool

Nonempty unary clock at every positive slice.

Equations

• seed.unary = List.replicate (m - seed.split) true

def Complexity.AuxiliaryUnarySeed.sample {m : ℕ} (seed : AuxiliaryUnarySeed m) : List Bool

Canonically encoded auxiliary-unary sample.

Equations

• seed.sample = Complexity.pair seed.binary seed.unary

def Complexity.FiniteEnsemble.auxiliaryUnary : FiniteEnsemble (List Bool)

Hirahara's uniform distribution with an auxiliary unary input, totalized at parameter zero.

Equations

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