Uniform binary strings

Uniform sampling from Fin n → Bool, represented as a list. The recursive equations connect this finite uniform distribution to a program drawing one independent fair bit at a time.

Main definitions

• Cslib.BitString.uniformList: uniform fixed-length words represented as lists.

Main results

• Cslib.BitString.uniformList_succ, Cslib.BitString.uniformList_add: independent decomposition.
• Cslib.BitString.mem_support_uniformList_iff: support is exactly the requested length.
• Cslib.BitString.uniformList_map_of_bijective: length-preserving permutations preserve uniformity.
• Cslib.BitString.uniformList_map_apply: the probability of a value under a map of a uniform word is the fraction of words of that length mapping to it.

References

Adapted from Cslib/Probability/BitString.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, placed in the shared bit-string namespace.

noncomputable def Cslib.BitString.uniformList (n : ℕ) : PMF (List Bool)

The uniform distribution on binary words of exactly n bits.

@[simp]

theorem Cslib.BitString.uniformList_zero : uniformList 0 = PMF.pure []

The uniform distribution on words of 0 bits is the point mass at the empty word.

theorem Cslib.BitString.uniformList_succ (n : ℕ) : uniformList (n + 1) = (Probability.PMF.uniformOfFintype Bool).bind fun (bit : Bool) => PMF.map (List.cons bit) (uniformList n)

A uniform nonempty string consists of a fair first bit and an independent uniform tail.

theorem Cslib.BitString.uniformList_add (m n : ℕ) : uniformList (m + n) = (uniformList m).bind fun (left : List Bool) => PMF.map (fun (x : List Bool) => left ++ x) (uniformList n)

Concatenating independent uniform words gives a uniform word of the combined length.

theorem Cslib.BitString.uniformList_snoc (n : ℕ) : uniformList (n + 1) = (uniformList n).bind fun (word : List Bool) => PMF.map (fun (bit : Bool) => word ++ [bit]) (Probability.PMF.uniformOfFintype Bool)

Appending one independent fair bit gives a uniform word one bit longer.

theorem Cslib.BitString.length_of_mem_support_uniformList {n : ℕ} {word : List Bool} (h : word ∈ (uniformList n).support) : word.length = n

Every sampled word has exactly the requested length.

theorem Cslib.BitString.mem_support_uniformList_iff {n : ℕ} {word : List Bool} : word ∈ (uniformList n).support ↔ word.length = n

Every word of the requested length has positive uniform probability, and no other word does.

theorem Cslib.BitString.uniformList_bind_split {α : Type u_1} (first second : ℕ) (next : List Bool → List Bool → PMF α) : ((uniformList (first + second)).bind fun (tape : List Bool) => next (List.take first tape) (List.drop first tape)) = (uniformList first).bind fun (front : List Bool) => (uniformList second).bind (next front)

Splitting a uniform tape gives two independent tapes, also when either length is zero.

theorem Cslib.BitString.uniformList_take {n k : ℕ} (hkn : k ≤ n) : PMF.map (List.take k) (uniformList n) = uniformList k

A prefix of a uniform word is uniform, with no condition on the discarded suffix.

theorem Cslib.BitString.uniformList_map_of_bijective (f : List Bool → List Bool) (hf : Function.Bijective f) (hlen : ∀ (word : List Bool), (f word).length = word.length) (n : ℕ) : PMF.map f (uniformList n) = uniformList n

A length-preserving permutation sends a uniform word to a uniform word of the same length. This is a distributional fact and makes no assumption about computing the inverse.

theorem Cslib.BitString.uniformList_map_apply {β : Type u_1} [DecidableEq β] (f : List Bool → β) (n : ℕ) (b : β) : (PMF.map f (uniformList n)) b = ↑{r : Fin n → Bool | f (List.ofFn r) = b}.card / 2 ^ n

The probability of a value of a function of a uniform word is the fraction of the words of that length giving it.