Documentation

Complexity.Foundations.Data.BitString.ShortWords

Counting binary words #

The binary words of length at most L form a finite set shortWords L with 2 ^ (L + 1) - 1 elements: the words of length m are the 2 ^ m lists List.ofFn r for r : Fin m → Bool, and ∑ m ≤ L, 2 ^ m = 2 ^ (L + 1) - 1. In particular, a list of fewer than 2 ^ n words leaves some word of length n unused.

Main definitions #

Main results #

source
theorem Cslib.BitString.encard_setOf_length_eq (n : ℕ) :
{p : List Bool | p.length = n}.encard = 2 ^ n

There are 2 ^ n binary strings of length n.

source
theorem Cslib.BitString.encard_setOf_length_lt_add_one (n : ℕ) :
{p : List Bool | p.length < n}.encard + 1 = 2 ^ n

There are 2 ^ n - 1 binary strings of length below n.

source
theorem Cslib.BitString.exists_length_eq_notMem (Q : List (List Bool)) (n : ℕ) (hQ : Q.length < 2 ^ n) :
∃ (w : List Bool), w.length = n ∧ w ∉ Q

Fewer than 2 ^ n words leave a word of length n unused.

source
noncomputable def Cslib.BitString.shortWords (L : ℕ) :
Finset (List Bool)

The binary words of length at most L.

Instances For
    source
    @[simp]
    theorem Cslib.BitString.mem_shortWords {L : ℕ} {w : List Bool} :
    w ∈ shortWords L ↔ w.length ≤ L

    A word lies in shortWords L exactly when its length is at most L.

    source
    theorem Cslib.BitString.nil_mem_shortWords (L : ℕ) :
    [] ∈ shortWords L

    The empty word lies in shortWords L.

    source
    theorem Cslib.BitString.card_shortWords (L : ℕ) :
    (shortWords L).card = 2 ^ (L + 1) - 1

    There are 2 ^ (L + 1) - 1 binary words of length at most L.

    source
    theorem Cslib.BitString.card_shortWords_lt (L : ℕ) :
    (shortWords L).card < 2 ^ (L + 1)

    There are fewer than 2 ^ (L + 1) binary words of length at most L.