Hamming weight and symmetric Boolean functions

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. The threshold function threshold n j says that at least j of n bits are true, and majority (majority, at least half) and strict majority (strictMajority, more than half) are threshold functions. A Boolean function is symmetric when it depends only on the weight of its input (BooleanFunction.IsSymmetric), and then it factors through the weight (BooleanFunction.IsSymmetric.exists_eq_comp_weight) Jukna, Chapter 1.

Main definitions

• Cslib.BitString.weight: the number of true coordinates, and Cslib.BitString.weightLayer the strings of a given weight.
• Cslib.threshold, Cslib.majority, Cslib.strictMajority: threshold functions.
• Cslib.BooleanFunction.IsSymmetric: Boolean functions depending only on the weight.

Main results

• Cslib.BitString.weight_eq_hammingNorm, Cslib.BitString.hammingDist_eq_weight_add: the weight is the Hamming norm.
• Cslib.BitString.monotone_weight, Cslib.monotone_threshold: the weight and threshold functions are monotone.
• Cslib.BitString.card_weightLayer: there are n.choose k strings of n bits of weight k.
• Cslib.BitString.card_filter_weight_le: the exact binomial-sum size of a Hamming ball.
• Cslib.BitString.card_image_le_sum_choose: bound a finite family of words by a Hamming ball.
• Cslib.strictMajority_not: strict majority of the negated bits is the negation of majority.
• Cslib.BitString.strictMajorityOn: strict majority on a finite set of voting indices.
• Cslib.le_card_ne_of_strictMajority_ne: a wrong majority requires at least half wrong votes.
• Cslib.isSymmetric_threshold: threshold functions are symmetric.

References

• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

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_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_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.

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.

def Cslib.BitString.strictMajorityOn {ι : Type u_1} (s : Finset ι) (vote : ι → Bool) : Bool

Strict majority of the coordinates in s, choosing false on a tie.

theorem Cslib.BitString.card_filter_eq_le_half_of_strictMajorityOn_ne {ι : Type u_1} (s : Finset ι) (vote : ι → Bool) (bit : Bool) (h : strictMajorityOn s vote ≠ bit) : {i ∈ s | vote i = bit}.card ≤ s.card / 2

If strict majority is wrong, at most half of the votes are correct.

@[simp]

theorem Cslib.BitString.strictMajorityOn_const {ι : Type u_1} (s : Finset ι) (hs : s.Nonempty) (bit : Bool) : (strictMajorityOn s fun (x : ι) => bit) = bit

A nonempty constant vote has its constant value.

def Cslib.threshold (n j : ℕ) : BooleanFunction n

The threshold function Th^n_j on n bits: whether at least j of them are true.

def Cslib.majority (n : ℕ) : BooleanFunction n

The majority function on n bits: whether at least half of them are true, that is, the threshold function Th^n_⌈n/2⌉.

def Cslib.strictMajority (n : ℕ) : BooleanFunction n

The strict majority function on n bits: whether more than half of them are true, so that a tie is false. It is the threshold function Th^n_{⌊n/2⌋+1}.

theorem Cslib.threshold_apply {n : ℕ} (j : ℕ) (x : BitString n) : threshold n j x = decide (j ≤ BitString.weight x)

threshold n j x is the decision of j ≤ weight x.

theorem Cslib.threshold_eq_true_iff {n j : ℕ} {x : BitString n} : threshold n j x = true ↔ j ≤ BitString.weight x

The threshold function Th^n_j is true exactly when at least j bits are true.

theorem Cslib.monotone_threshold {n : ℕ} (j : ℕ) : Monotone (threshold n j)

Threshold functions are monotone.

@[simp]

theorem Cslib.threshold_zero_right {n : ℕ} (x : BitString n) : threshold n 0 x = true

With cutoff 0, the threshold function is the constant true.

theorem Cslib.threshold_eq_false_of_lt {n j : ℕ} (h : n < j) (x : BitString n) : threshold n j x = false

With a cutoff above n, the threshold function is the constant false.

theorem Cslib.threshold_one_right {n : ℕ} (x : BitString n) : threshold n 1 x = decide (∃ (i : Fin n), x i = true)

With cutoff 1, the threshold function is the disjunction.

theorem Cslib.threshold_self {n : ℕ} (x : BitString n) : threshold n n x = decide (∀ (i : Fin n), x i = true)

With cutoff n, the threshold function is the conjunction.

theorem Cslib.majority_eq_true_iff {n : ℕ} {x : BitString n} : majority n x = true ↔ (n + 1) / 2 ≤ BitString.weight x

Majority is true exactly when at least ⌈n/2⌉ = (n + 1) / 2 bits are true.

theorem Cslib.strictMajority_eq_true_iff {n : ℕ} {x : BitString n} : strictMajority n x = true ↔ n / 2 < BitString.weight x

Strict majority is true exactly when more than n / 2 bits are true.

theorem Cslib.strictMajority_eq_false_iff {n : ℕ} {x : BitString n} : strictMajority n x = false ↔ BitString.weight x ≤ n / 2

Strict majority is false exactly when at most n / 2 bits are true.

theorem Cslib.strictMajority_eq_strictMajorityOn {n : ℕ} (x : BitString n) : strictMajority n x = BitString.strictMajorityOn Finset.univ x

Strict majority on all coordinates agrees with the finite-set operation.

theorem Cslib.le_card_ne_of_strictMajority_ne {n : ℕ} {x : BitString n} {y : Bool} (h : strictMajority n x ≠ y) : n - n / 2 ≤ {i : Fin n | x i ≠ y}.card

If the strict majority of n bits is not y, at least n - n / 2 differ from y.

theorem Cslib.strictMajority_not {n : ℕ} (x : BitString n) : (strictMajority n fun (i : Fin n) => !x i) = !majority n x

Strict majority of the negated bits is the negation of majority: fewer than half of the bits are true exactly when not at least half of them are.

def Cslib.BooleanFunction.IsSymmetric {n : ℕ} (f : BooleanFunction n) : Prop

A Boolean function is symmetric when it depends only on the weight of its input.

theorem Cslib.BooleanFunction.IsSymmetric.exists_eq_comp_weight {n : ℕ} {f : BooleanFunction n} (hf : f.IsSymmetric) : ∃ (a : ℕ → Bool), ∀ (x : Fin n → Bool), a (BitString.weight x) = f x

A symmetric function factors through the weight.

theorem Cslib.isSymmetric_threshold {n : ℕ} (j : ℕ) : (threshold n j).IsSymmetric

Threshold functions are symmetric.

theorem Cslib.isSymmetric_majority {n : ℕ} : (majority n).IsSymmetric

Majority is symmetric.

theorem Cslib.isSymmetric_strictMajority {n : ℕ} : (strictMajority n).IsSymmetric

Strict majority is symmetric.