Cover's enumerative coding for weight-bounded Boolean words

Cover's lexicographic rank (Cslib.BitString.coverRank) and greedy threshold decoder (Cslib.BitString.coverDecode) establish an explicit bijection between words z : Fin q → Bool of Hamming weight at most e and indices below the Hamming-ball size B(q, e) = ∑ j ∈ range (e + 1), q.choose j (Cslib.BitString.ballSize).

Main definitions

• Cslib.BitString.ballSize: the size ∑ j ∈ range (e + 1), q.choose j of the binary Hamming ball of radius e in Fin q → Bool.
• Cslib.BitString.coverRank: Cover's lexicographic rank of a weight-bounded Boolean word.
• Cslib.BitString.coverDecode: Cover's greedy threshold decoder recovering a word of weight at most e from its rank below ballSize q e.

Main results

• Cslib.BitString.ballSize_succ_succ: Pascal recurrence for Hamming-ball sizes.
• Cslib.BitString.card_filter_weight_le_eq_ballSize: the number of words in Fin q → Bool of weight at most e equals ballSize q e.
• Cslib.BitString.coverRank_lt_ballSize, Cslib.BitString.weight_coverDecode_le, Cslib.BitString.coverRank_coverDecode, Cslib.BitString.coverDecode_coverRank: mutual inverse and weight bounds for Cover's enumerative coding.

References

• [T. M. Cover, Enumerative source encoding][Cover1973]
• [Threshold Circuits as Decision Trees and Finite-State Programs, Section 4] [26]

def Cslib.BitString.ballSize (q e : ℕ) : ℕ

Size B(q, e) = ∑ j ∈ range (e + 1), q.choose j of the Hamming ball of radius e in {0, 1}^q.

@[simp]

theorem Cslib.BitString.ballSize_zero_left (e : ℕ) : ballSize 0 e = 1

The Hamming ball of any radius in the cube of dimension 0 has one point.

@[simp]

theorem Cslib.BitString.ballSize_zero_right (q : ℕ) : ballSize q 0 = 1

The Hamming ball of radius 0 has one point.

theorem Cslib.BitString.ballSize_pos (q e : ℕ) : 0 < ballSize q e

Hamming balls are nonempty: 0 < ballSize q e.

theorem Cslib.BitString.ballSize_succ_succ (q e : ℕ) : ballSize (q + 1) (e + 1) = ballSize q (e + 1) + ballSize q e

Pascal recurrence B(q + 1, e + 1) = B(q, e + 1) + B(q, e) for Hamming-ball sizes.

theorem Cslib.BitString.card_filter_weight_le_eq_ballSize (q e : ℕ) : {z : Fin q → Bool | weight z ≤ e}.card = ballSize q e

The number of words z : Fin q → Bool of weight at most e equals ballSize q e.

def Cslib.BitString.coverRank {q : ℕ} : ℕ → (Fin q → Bool) → ℕ

Cover's lexicographic rank of a word z : Fin q → Bool among words of weight at most e.

def Cslib.BitString.coverDecode (q e t : ℕ) : Fin q → Bool

Cover's greedy threshold decoder recovering a word z : Fin q → Bool of weight at most e from its rank t < ballSize q e.

theorem Cslib.BitString.weight_cons_succ {q : ℕ} (z : Fin (q + 1) → Bool) : weight z = (z 0).toNat + weight fun (i : Fin q) => z i.succ

Splitting off the first bit of a word z : Fin (q + 1) → Bool in its Hamming weight.

theorem Cslib.BitString.coverRank_lt_ballSize {q : ℕ} (e : ℕ) (z : Fin q → Bool) (hz : weight z ≤ e) : coverRank e z < ballSize q e

Every word z : Fin q → Bool of weight at most e has coverRank e z < ballSize q e.

theorem Cslib.BitString.weight_coverDecode_le (q e t : ℕ) : weight (coverDecode q e t) ≤ e

Every decoded word coverDecode q e t has Hamming weight at most e.

@[simp]

theorem Cslib.BitString.coverRank_coverDecode {q e t : ℕ} (ht : t < ballSize q e) : coverRank e (coverDecode q e t) = t

Ranking a decoded word coverDecode q e t for t < ballSize q e recovers t.

@[simp]

theorem Cslib.BitString.coverDecode_coverRank {q e : ℕ} (z : Fin q → Bool) (hz : weight z ≤ e) : coverDecode q e (coverRank e z) = z

Decoding the rank coverRank e z of a word z : Fin q → Bool with weight z ≤ e recovers z.