Hamming weight and binary Hamming balls

The weight of a Boolean vector is its number of true coordinates (BitString.weight), Mathlib's Hamming norm with false as 0 (BitString.weight_eq_hammingNorm), so the Hamming distance of two bit strings is the weight of their sum (BitString.hammingDist_eq_weight_add) MacWilliams and Sloane, Chapter 1. For x : BitString n, the weight is the number of true entries of List.ofFn x (BitString.count_true_ofFn) and is at most n (BitString.weight_le_length). The words of weight k in BitString n form the k-th layer of the cube (BitString.weightLayer), of size n.choose k (BitString.card_weightLayer), and the words of weight at most e form a Hamming ball of size B(n, e) = ∑ j ∈ range (e + 1), n.choose j (BitString.ballSize, BitString.card_filter_weight_le, BitString.card_filter_weight_le_eq_ballSize).

Main definitions

• Cslib.BitString.weight: the number of true coordinates.
• Cslib.BitString.weightLayer: the strings of n bits of a given weight.
• Cslib.BitString.ballSize: the size ∑ j ∈ range (e + 1), q.choose j of the binary Hamming ball of radius e in BitString q.

Main results

• Cslib.BitString.weight_eq_hammingNorm, Cslib.BitString.hammingDist_eq_weight_add: the weight is the Hamming norm.
• Cslib.BitString.weight_le, Cslib.BitString.weight_le_length: the weight is at most the number of coordinates.
• Cslib.BitString.count_true_ofFn: (List.ofFn x).count true = weight x.
• Cslib.BitString.monotone_weight: the weight is monotone.
• Cslib.BitString.card_weightLayer: there are n.choose k strings of n bits of weight k.
• Cslib.BitString.card_filter_weight_le, Cslib.BitString.card_filter_weight_le_eq_ballSize: the exact binomial-sum size of a Hamming ball.
• Cslib.BitString.ballSize_succ_succ: Pascal recurrence for Hamming-ball sizes.
• Cslib.BitString.card_image_le_sum_choose: bound a finite family of words by a Hamming ball.

References

• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

def Cslib.BitString.weight {ι : Type u_1} [Fintype ι] (x : ι → Bool) : ℕ

The Hamming weight of a Boolean vector: its number of true coordinates.

theorem Cslib.BitString.weight_eq_sum_toNat {ι : Type u_1} [Fintype ι] (x : ι → Bool) : weight x = ∑ i : ι, (x i).toNat

The weight is the sum of the bits read as 0 and 1.

theorem Cslib.BitString.weight_eq_hammingNorm {ι : Type u_1} [Fintype ι] (x : ι → Bool) : weight x = hammingNorm x

The weight is Mathlib's Hamming norm, the bit false being 0.

theorem Cslib.BitString.hammingDist_eq_weight_add {ι : Type u_1} [Fintype ι] (x y : ι → Bool) : hammingDist x y = weight (x + y)

The Hamming distance between two bit strings is the weight of their sum.

theorem Cslib.BitString.weight_le {ι : Type u_1} [Fintype ι] (x : ι → Bool) : weight x ≤ Fintype.card ι

The weight is at most the number of coordinates.

theorem Cslib.BitString.weight_le_length {n : ℕ} (x : BitString n) : weight x ≤ n

The weight of an n-bit string is at most n.

theorem Cslib.BitString.weight_not_add {ι : Type u_1} [Fintype ι] (x : ι → Bool) : (weight fun (i : ι) => !x i) + weight x = Fintype.card ι

Complementary vectors have weights adding up to the number of coordinates.

theorem Cslib.BitString.weight_not {ι : Type u_1} [Fintype ι] (x : ι → Bool) : (weight fun (i : ι) => !x i) = Fintype.card ι - weight x

The weight of the complement is the number of coordinates minus the weight.

theorem Cslib.BitString.card_filter_eq_false_eq_card_sub_weight {ι : Type u_1} [Fintype ι] (x : ι → Bool) : {i : ι | x i = false}.card = Fintype.card ι - weight x

The false coordinates of x number the coordinates minus the weight.

theorem Cslib.BitString.monotone_weight {ι : Type u_1} [Fintype ι] : Monotone weight

The weight is monotone in the pointwise order: setting bits cannot lower it.

@[simp]

theorem Cslib.BitString.weight_sum_elim {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (x : ι → Bool) (y : κ → Bool) : weight (Sum.elim x y) = weight x + weight y

The weight of a vector on ι ⊕ κ glued from x and y is the sum of their weights.

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.

@[simp]

theorem Cslib.BitString.count_true_ofFn {n : ℕ} (x : BitString n) : List.count true (List.ofFn x) = weight x

The number of true entries in List.ofFn x is the weight of x.

theorem Cslib.BitString.weight_update_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] {x : ι → Bool} {i : ι} (hi : x i = false) : weight (Function.update x i true) = weight x + 1

Setting a false coordinate to true adds one to the weight.

theorem Cslib.BitString.weight_update_false {ι : Type u_1} [Fintype ι] [DecidableEq ι] {x : ι → Bool} {i : ι} (hi : x i = true) : weight (Function.update x i false) + 1 = weight x

Setting a true coordinate to false takes one from the weight.

theorem Cslib.BitString.card_filter_weight_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : ℕ) : {x : ι → Bool | weight x = r}.card = (Fintype.card ι).choose r

The words ι → Bool of weight r number |ι|.choose r: they are the indicators of the r-element sets of coordinates.

theorem Cslib.BitString.card_filter_weight_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (e : ℕ) : {x : ι → Bool | weight x ≤ e}.card = ∑ j ∈ Finset.range (e + 1), (Fintype.card ι).choose j

The words of weight at most e form a Hamming ball with the exact binomial-sum size. The radius may exceed the number of coordinates.

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.

theorem Cslib.BitString.weight_eq_card_subtype {ι : Type u_1} [Fintype ι] (x : ι → Bool) : weight x = Fintype.card { i : ι // x i = true }

The weight of x as a number of true coordinates.

theorem Cslib.BitString.weight_comp_le {ι : Type u_1} [Fintype ι] {κ : Type u_2} [Fintype κ] (x : ι → Bool) {f : κ → ι} (hf : Function.Injective f) : weight (x ∘ f) ≤ weight x

Selecting distinct coordinates cannot increase the number of true bits.

theorem Cslib.BitString.card_image_le_sum_choose {ι : Type u_1} [Fintype ι] {α : Type u_2} (s : Finset α) (f : α → ι → Bool) {e : ℕ} (h : ∀ x ∈ s, weight (f x) ≤ e) : (Finset.image f s).card ≤ ∑ j ∈ Finset.range (e + 1), (Fintype.card ι).choose j

A finite family of words of weight at most e attains at most the Hamming-ball size. The map need not be injective, and the radius may exceed the number of coordinates.

def Cslib.BitString.weightLayer (n k : ℕ) : Finset (BitString n)

The layer of weight k of the cube: the strings of n bits with k true bits.

@[simp]

theorem Cslib.BitString.mem_weightLayer {n k : ℕ} {x : BitString n} : x ∈ weightLayer n k ↔ weight x = k

A string lies in the layer of weight k exactly when its weight is k.

theorem Cslib.BitString.card_weightLayer (n k : ℕ) : (weightLayer n k).card = n.choose k

The layer of weight k has n.choose k strings.

theorem Cslib.BitString.weightLayer_nonempty {n k : ℕ} (hk : k ≤ n) : (weightLayer n k).Nonempty

The layer of weight k of the cube of n bits is nonempty when k ≤ n.