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, Cslib.BitString.toOuterMeasure_map_uniformList_toReal: the probability of a value or event under a map of a uniform word is the fraction of words of that length mapping into it.
• Cslib.BitString.uniformList_apply_le, Cslib.BitString.toOuterMeasure_uniformList_finset_le, Cslib.BitString.toOuterMeasure_lookup_uniformList_le: point-mass bound 1 / 2 ^ n, finite-set union bound s.card * (1 / 2 ^ n), and finite-cache lookup union bound cache.length * (1 / 2 ^ n) for uniformList n.

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.

theorem Cslib.BitString.toOuterMeasure_map_uniformList_toReal {β : Type u_1} (f : List Bool → β) (n : ℕ) (S : Set β) : ((PMF.map f (uniformList n)).toOuterMeasure S).toReal = ↑{r : Fin n → Bool | f (List.ofFn r) ∈ S}.card / 2 ^ n

The real probability that a function of a uniform word of length n lands in S is the fraction of words of that length mapping into S.

theorem Cslib.BitString.uniformList_apply_le (n : ℕ) (r : List Bool) : (uniformList n) r ≤ 1 / 2 ^ n

Every candidate word r has probability at most 1 / 2 ^ n under uniformList n.

theorem Cslib.BitString.toOuterMeasure_uniformList_finset_le (n : ℕ) (s : Finset (List Bool)) : (uniformList n).toOuterMeasure ↑s ≤ ↑s.card * (1 / 2 ^ n)

Union bound on finite candidate sets: a uniform n-bit word lands in a finite set s with outer measure at most s.card * (1 / 2 ^ n).

theorem Cslib.BitString.toOuterMeasure_lookup_uniformList_le {V : Type u_1} (n : ℕ) (cache : List (List Bool × V)) : (uniformList n).toOuterMeasure {r : List Bool | (List.lookup r cache).isSome = true} ≤ ↑cache.length * (1 / 2 ^ n)

Union bound on finite-cache lookups: a uniform n-bit word hits the domain of a finite association list cache with outer measure at most cache.length * (1 / 2 ^ n).