Counting words

Counting the words List.ofFn v, for v : Fin n → Bool, that pass a test: the counting arguments of parity and counting classes, which count accepted certificates. A word of length m + n is a prefix of length m followed by a word of length n (Cslib.BitString.card_filter_ofFn_add); a word of length n + 1 is a first bit followed by a word of length n (Cslib.BitString.card_filter_ofFn_succ); a word of T rows of B bits whose rows pass independent tests is counted by a product (Cslib.BitString.card_filter_listRows_all). Exactly one word has no bit true, and exactly one has no bit false (Cslib.BitString.card_filter_not_any, Cslib.BitString.card_filter_all).

The lexicographic order on words of equal length (Cslib.BitString.wordLt) is the order of Lex (Fin n → Bool) (Cslib.BitString.wordLt_ofFn_iff), so strictly increasing lists of words represent sets of words.

Main definitions

• Cslib.BitString.wordLt: the lexicographic order on words of equal length.

Main results

• Cslib.BitString.card_filter_binaryValue_lt: exact counts below a binary threshold.
• Cslib.BitString.card_filter_ofFn_add, Cslib.BitString.card_filter_ofFn_succ: counting words by a prefix or by their first bit.
• Cslib.BitString.card_filter_take: counting words by a condition on a prefix.
• Cslib.BitString.card_filter_take_drop: independent prefix/suffix tests give a product.
• Cslib.BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le: a quarter of failures leaves two thirds of successes.
• Cslib.BitString.two_pow_mul_card_filter_card_filter_block_le: majority votes of 12 e blocks err on at most a 2 ^ (-e) fraction.
• Cslib.BitString.card_filter_listRows_all: counting words by a condition on each row.
• Cslib.BitString.card_filter_not_any, Cslib.BitString.card_filter_all: the constant words.
• Cslib.BitString.ofFn_decide_lt: the unary word of k bits true among K.
• Cslib.BitString.wordLt_ofFn_iff: wordLt is the lexicographic order.
• Cslib.BitString.odd_prod_iff, Cslib.BitString.odd_one_add_prod_one_add: parity of products and the parity form of a disjunction.
• Cslib.BitString.card_filter_forall_apply_mem: counting functions with restricted values on an injective family of points.
• Cslib.BitString.two_pow_mul_card_filter_exists_le: union bound for random strings.
• Cslib.BitString.sum_range_neg_two_pow_mul_choose, Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod: the parity of c from binomial coefficients, over ℤ and modulo 2 ^ K.
• Cslib.BitString.card_filter_strictMono, Cslib.BitString.strictMono_of_lt_succ: strictly increasing tuples count subsets.

Counting words

theorem Cslib.BitString.card_filter_ofFn_add (m n : ℕ) (g : List Bool → List Bool → Prop) [(u w : List Bool) → Decidable (g u w)] : {v : Fin (m + n) → Bool | g (List.take m (List.ofFn v)) (List.drop m (List.ofFn v))}.card = ∑ u : Fin m → Bool, {w : Fin n → Bool | g (List.ofFn u) (List.ofFn w)}.card

Counting words by their prefixes: the words of length m + n are the words u ++ w with u of length m and w of length n.

theorem Cslib.BitString.card_filter_take {k K : ℕ} (h : k ≤ K) (g : List Bool → Prop) [DecidablePred g] : {r : Fin K → Bool | g (List.take k (List.ofFn r))}.card = 2 ^ (K - k) * {r : Fin k → Bool | g (List.ofFn r)}.card

Counting words by a prefix. For k ≤ K, the words of K bits whose prefix of length k satisfies g are 2 ^ (K - k) times as many as the words of k bits satisfying g.

theorem Cslib.BitString.card_filter_take_drop {m a : ℕ} (h : a ≤ m) (P Q : List Bool → Prop) [DecidablePred P] [DecidablePred Q] : {r : Fin m → Bool | P (List.take a (List.ofFn r)) ∧ Q (List.drop a (List.ofFn r))}.card = {u : Fin a → Bool | P (List.ofFn u)}.card * {v : Fin (m - a) → Bool | Q (List.ofFn v)}.card

Counting words of length m by a condition on their first a bits and a condition on the remaining bits gives the product of the two counts.

theorem Cslib.BitString.two_mul_two_pow_le_of_four_mul_card_filter_not_le {m : ℕ} (g : BitString m → Prop) [DecidablePred g] (h : 4 * {r : BitString m | ¬g r}.card ≤ 2 ^ m) : 2 * 2 ^ m ≤ 3 * {r : BitString m | g r}.card

Error at most 1 / 4 is error at most 1 / 3: if at most a quarter of the strings of m bits fail g, at least two thirds of them satisfy it.

theorem Cslib.BitString.two_pow_mul_card_filter_card_filter_block_le {m e R : ℕ} (hR : R = 6 * e) (g : BitString m → Prop) [DecidablePred g] (hg : 2 * 2 ^ m ≤ 3 * {s : BitString m | g s}.card) : 2 ^ e * {x : BitString (2 * R * m) | {i : Fin (2 * R) | g (x.block i)}.card ≤ R}.card ≤ 2 ^ (2 * R * m)

Majority votes of blocks. If at least two thirds of the strings of m bits satisfy g, then at most a 2 ^ (-e) fraction of the strings of 2 R = 12 e blocks of m bits have at most R blocks satisfying g: the exponential-moment bound Cslib.card_filter_card_filter_le_le, with 2 * 8 ^ 6 ≤ 9 ^ 6.

theorem Cslib.BitString.card_filter_ofFn_succ (n : ℕ) (g : List Bool → Prop) [DecidablePred g] : {v : Fin (n + 1) → Bool | g (List.ofFn v)}.card = {w : Fin n → Bool | g (true :: List.ofFn w)}.card + {w : Fin n → Bool | g (false :: List.ofFn w)}.card

Counting words by their first bit.

theorem Cslib.BitString.card_filter_not_any (n : ℕ) : {w : Fin n → Bool | (!(List.ofFn w).any fun (b : Bool) => b) = true}.card = 1

Only the word of falses has no bit true.

theorem Cslib.BitString.card_filter_all (n : ℕ) : {w : Fin n → Bool | ((List.ofFn w).all fun (b : Bool) => b) = true}.card = 1

Only the word of trues has all bits true.

theorem Cslib.BitString.card_filter_listRows_all (T B : ℕ) (g : ℕ → List Bool → Bool) : {v : Fin (T * B) → Bool | ((listRows T B (List.ofFn v)).zipIdx.all fun (p : List Bool × ℕ) => g p.2 p.1) = true}.card = ∏ j : Fin T, {w : Fin B → Bool | g (↑j) (List.ofFn w) = true}.card

Counting words by rows: the words of T rows of B bits whose j-th row satisfies g j for every j are counted by the product of the counts of the rows.

theorem Cslib.BitString.ofFn_decide_lt {K k : ℕ} (hk : k ≤ K) : (List.ofFn fun (i : Fin K) => decide (↑i < k)) = List.replicate k true ++ List.replicate (K - k) false

The unary word of k ≤ K bits true followed by falses.

The lexicographic order

def Cslib.BitString.wordLt (x y : List Bool) : Bool

The lexicographic order on words of equal length: x is below y at the first position where they differ.

theorem Cslib.BitString.wordLt_ofFn_iff {n : ℕ} (x y : Fin n → Bool) : wordLt (List.ofFn x) (List.ofFn y) = true ↔ toLex x < toLex y

On bit strings, wordLt is the lexicographic order.

theorem Cslib.BitString.card_filter_binaryValue_lt {n k : ℕ} (hk : k ≤ 2 ^ n) : {w : Fin n → Bool | binaryValue (List.ofFn w) < k}.card = k

Among all n-bit words, precisely k represent values below k ≤ 2^n.

Parity, subsets, and binomial amplification

theorem Cslib.BitString.odd_prod_iff {ι : Type u_1} {s : Finset ι} (f : ι → ℕ) : Odd (∏ j ∈ s, f j) ↔ ∀ j ∈ s, Odd (f j)

A product of naturals is odd exactly when every factor is.

theorem Cslib.BitString.odd_one_add_prod_one_add {ι : Type u_1} [Fintype ι] (c : ι → ℕ) : Odd (1 + ∏ j : ι, (1 + c j)) ↔ ∃ (j : ι), Odd (c j)

The parity form of a disjunction: 1 + ∏ⱼ (1 + cⱼ) is odd exactly when some cⱼ is odd.

theorem Cslib.BitString.card_filter_forall_apply_mem {ι : Type u_1} {X : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype X] [DecidableEq X] {t : ℕ} (f : Fin t → ι) (hf : Function.Injective f) (F : Finset X) : {s : ι → X | ∀ (i : Fin t), s (f i) ∈ F}.card = F.card ^ t * Fintype.card X ^ (Fintype.card ι - t)

The functions s : ι → X whose values at the t distinct points f i lie in F: F is chosen at those points and anything elsewhere.

theorem Cslib.BitString.two_pow_mul_card_filter_exists_le {R M e' : ℕ} {Bad : (Fin R → Bool) → (Fin M → Bool) → Prop} [(r : Fin R → Bool) → (x : Fin M → Bool) → Decidable (Bad r x)] (h : ∀ (x : Fin M → Bool), 2 ^ e' * {r : Fin R → Bool | Bad r x}.card ≤ 2 ^ R) : 2 ^ e' * {r : Fin R → Bool | ∃ (x : Fin M → Bool), Bad r x}.card ≤ 2 ^ M * 2 ^ R

The union bound for random strings: if each x is bad for at most a 2 ^ (-e') fraction of the random strings, some x of length M is bad for at most a 2 ^ (M - e') fraction.

theorem Cslib.BitString.sum_range_neg_two_pow_mul_choose (c : ℕ) : ∑ i ∈ Finset.range c, (-2) ^ i * ↑(c.choose (i + 1)) = if Odd c then 1 else 0

The parity of c from the binomial expansion of (1 - 2) ^ c: ∑ i < c, (-2) ^ i * choose c (i + 1) is 1 for odd c and 0 for even c.

theorem Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod (c K : ℕ) : ∑ i ∈ Finset.range K, (-2) ^ i * ↑(c.choose (i + 1)) = if Odd c then 1 else 0

The parity of c modulo 2 ^ K: only the first K binomial terms matter.

theorem Cslib.BitString.card_filter_strictMono {β : Type u_1} [LinearOrder β] [Fintype β] (A : Finset β) (k : ℕ) [DecidablePred fun (g : Fin k → β) => StrictMono g ∧ ∀ (i : Fin k), g i ∈ A] : {g : Fin k → β | StrictMono g ∧ ∀ (i : Fin k), g i ∈ A}.card = A.card.choose k

Strictly increasing tuples count subsets: the strictly increasing k-tuples of elements of A are as many as the k-element subsets of A.

theorem Cslib.BitString.strictMono_of_lt_succ {β : Type u_1} [Preorder β] {k : ℕ} {g : Fin k → β} (h : ∀ (i : ℕ) (hi : i + 1 < k), g ⟨i, ⋯⟩ < g ⟨i + 1, hi⟩) : StrictMono g

A tuple increasing at every step is strictly increasing.