The auxiliary-unary distribution -- proof internals

This layer proves the exact shape and finite counting laws of Hirahara's auxiliary-unary distribution.

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

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

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

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

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

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

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

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

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

theorem Complexity.AuxiliaryUnarySeed.split_prefix_event_probability_internal {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)

theorem Complexity.AuxiliaryUnarySeed.split_prefix_probability_internal {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)

theorem Complexity.AuxiliaryUnarySeed.sample_eq_pair_iff_internal {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

theorem Complexity.FiniteEnsemble.mass_auxiliaryUnary_pair_internal {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)