The auxiliary-unary distribution

This module exposes the exact sampler shape and counting theory for Hirahara's uniform distribution with auxiliary unary input. At positive parameter m, a sample is pair x (List.replicate t true) for uniform t ∈ {1, ..., m} and uniform x ∈ {0,1}^{m-t}.

theorem Complexity.AuxiliaryUnarySeed.split_lt {m : ℕ} (hm : 0 < m) (seed : AuxiliaryUnarySeed m) : seed.split < m

The selected binary length is strictly below every positive slice parameter.

@[simp]

theorem Complexity.AuxiliaryUnarySeed.binary_length {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.binary.length = seed.split

The retained binary component has the selected length.

@[simp]

theorem Complexity.AuxiliaryUnarySeed.unary_length {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.unary.length = m - seed.split

The unary component fills the remainder of the size parameter.

theorem Complexity.AuxiliaryUnarySeed.unary_length_pos {m : ℕ} (hm : 0 < m) (seed : AuxiliaryUnarySeed m) : 0 < seed.unary.length

The auxiliary unary clock is nonempty on every positive slice.

theorem Complexity.AuxiliaryUnarySeed.component_length_sum {m : ℕ} (seed : AuxiliaryUnarySeed m) : seed.binary.length + seed.unary.length = m

The two decoded component lengths sum to the slice parameter.

@[simp]

theorem Complexity.AuxiliaryUnarySeed.unpair?_sample {m : ℕ} (seed : AuxiliaryUnarySeed m) : unpair? seed.sample = some (seed.binary, seed.unary)

Decoding an auxiliary-unary sample recovers its two components exactly.

theorem Complexity.AuxiliaryUnarySeed.card (m : ℕ) : Fintype.card (AuxiliaryUnarySeed m) = Nat.max 1 m * 2 ^ m

The mth seed space contains max 1 m * 2^m equiprobable seeds.

theorem Complexity.AuxiliaryUnarySeed.prefix_probability {m n : ℕ} (hn : n ≤ m) (x : Fin n → Bool) : uniformProbability {bits : Fin m → Bool | ((bitBlocks hn) bits).1 = x} = 1 / 2 ^ n

A uniform m-bit string has any fixed length-n prefix with probability exactly 2^-n.

theorem Complexity.AuxiliaryUnarySeed.prefix_event_probability {m n : ℕ} (hn : n ≤ m) (event : Finset (Fin n → Bool)) : uniformProbability {bits : Fin m → Bool | ((bitBlocks hn) bits).1 ∈ event} = eventProb event

Retaining a uniform prefix preserves the exact uniform probability of every finite event on prefixes, not only singleton events.

theorem Complexity.AuxiliaryUnarySeed.split_prefix_event_probability {m : ℕ} (event : (n : ℕ) → Finset (Fin n → Bool)) : uniformProbability {seed : Fin m × (Fin m → Bool) | ((bitBlocks ⋯) seed.2).1 ∈ event ↑seed.1} = 1 / ↑m * ∑ n : Fin m, eventProb (event ↑n)

Choosing a split and retaining its prefix gives the uniform average of a possibly length-dependent family of prefix-event probabilities.

theorem Complexity.AuxiliaryUnarySeed.split_prefix_probability {m n : ℕ} (hn : n < m) (x : Fin n → Bool) : uniformProbability {seed : AuxiliaryUnarySeed m | ↑seed.1 = n ∧ ((bitBlocks ⋯) seed.2).1 = x} = 1 / (↑m * 2 ^ n)

The joint seed event selecting binary length n and fixed prefix x has probability exactly 1 / (m * 2^n).

theorem Complexity.AuxiliaryUnarySeed.sample_eq_pair_iff {m n : ℕ} (hn : n < m) (x : Fin n → Bool) (seed : AuxiliaryUnarySeed m) : seed.sample = pair (List.ofFn x) (List.replicate (m - n) true) ↔ ↑seed.1 = n ∧ ((bitBlocks ⋯) seed.2).1 = x

A seed produces a specified canonical auxiliary-unary pair exactly when it selects the pair's binary length and binary contents.

theorem Complexity.FiniteEnsemble.mass_auxiliaryUnary_pair {m n : ℕ} (hn : n < m) (x : Fin n → Bool) : auxiliaryUnary.mass m (pair (List.ofFn x) (List.replicate (m - n) true)) = 1 / (↑m * 2 ^ n)

Exact mass of a fixed auxiliary-unary input. For n < m, every pair x 1^(m-n) with |x| = n has probability 1 / (m * 2^n).