Weight distributions and weight enumerators

For a set of words C on a finite coordinate type ι of size n, the weight distribution A_w(C) counts the words of Hamming weight w, and the homogeneous weight enumerator is

W_C(X, Y) = ∑_w A_w(C) X^(n-w) Y^w,

which for finite C equals the sum over codewords ∑_{c ∈ C} X^(n - wt c) Y^(wt c). It is a homogeneous polynomial of degree n with integer coefficients, with the variables 0, 1 of MvPolynomial (Fin 2) ℤ playing the roles of X, Y. Its one-variable specialization at X = 1 is the weight polynomial ∑_w A_w(C) Y^w, of degree at most n.

These invariants carry the Hamming data of a finite code in the form used by the MacWilliams identity #C · W_{C⊥}(X, Y) = W_C(X + (q - 1) Y, X - Y): they are unchanged by monomial equivalence and recover the cardinality and minimum distance of a finite additive code.

Main definitions

• Set.weightDistribution C w: the number of words of C of Hamming weight w.
• Set.weightEnumerator C: the homogeneous weight enumerator W_C(X, Y).
• Set.weightPolynomial C: the one-variable weight enumerator W_C(1, Y).

Main statements

• Set.weightEnumerator_eq_sum: W_C is the sum over codewords of X^(n - wt c) Y^(wt c).
• Set.coeff_weightEnumerator, Set.coeff_weightPolynomial: the coefficients are the weight distribution.
• Set.isHomogeneous_weightEnumerator, Set.eval_one_weightEnumerator: W_C is homogeneous of degree n, and W_C(1, 1) = #C.
• Set.hammingMinDist_eq_sInf_weightDistribution: the minimum distance of a finite additive code is its least positive weight with nonzero multiplicity.
• TauCeti.IsMonomialEquivalent.weightEnumerator_eq: monomially equivalent codes have the same weight enumerator.

References

W. C. Huffman and V. Pless, Fundamentals of Error-Correcting Codes, Cambridge University Press (2003), §7.2; F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland (1977), Chapter 5, §2.

The weight distribution

noncomputable def Set.weightDistribution {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) (w : ℕ) : ℕ

The weight distribution of a set of words: the number of words of Hamming weight w. It is meaningful for finite sets of words; for an infinite fibre Nat.card is zero.

theorem Set.weightDistribution_def {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) (w : ℕ) : C.weightDistribution w = Nat.card { x : (i : ι) → β i // x ∈ C ∧ hammingNorm x = w }

theorem Set.weightDistribution_eq_card_filter {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) (w : ℕ) : C.weightDistribution w = {x ∈ hC.toFinset | hammingNorm x = w}.card

For a finite set of words, the weight distribution counts a finite filter.

theorem Set.weightDistribution_eq_zero_of_card_lt {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {w : ℕ} (hw : Fintype.card ι < w) : C.weightDistribution w = 0

There are no words of weight greater than the length.

@[simp]

theorem Set.weightDistribution_zero {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (h : 0 ∈ C) : C.weightDistribution 0 = 1

A set of words containing the zero word has exactly one word of weight zero.

theorem Set.weightDistribution_ne_zero_iff {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) {w : ℕ} : C.weightDistribution w ≠ 0 ↔ ∃ x ∈ C, hammingNorm x = w

In a finite set of words, a weight occurs exactly when some word has that weight.

theorem Set.sum_weightDistribution {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) : ∑ w ∈ Finset.range (Fintype.card ι + 1), C.weightDistribution w = Nat.card ↑C

The weight distribution of a finite set of words sums to its cardinality.

The homogeneous weight enumerator

noncomputable def Set.weightEnumerator {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : MvPolynomial (Fin 2) ℤ

The homogeneous Hamming weight enumerator W_C(X, Y) = ∑_w A_w(C) X^(n-w) Y^w, where n is the length, A_w(C) is the weight distribution, and the variables 0, 1 are X, Y.

theorem Set.weightEnumerator_def {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.weightEnumerator = ∑ w ∈ Finset.range (Fintype.card ι + 1), MvPolynomial.C ↑(C.weightDistribution w) * MvPolynomial.X 0 ^ (Fintype.card ι - w) * MvPolynomial.X 1 ^ w

theorem Set.weightEnumerator_eq_sum {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) : C.weightEnumerator = ∑ c ∈ hC.toFinset, MvPolynomial.X 0 ^ (Fintype.card ι - hammingNorm c) * MvPolynomial.X 1 ^ hammingNorm c

The weight enumerator of a finite set of words is the sum over its words c of X^(n - wt c) Y^(wt c).

theorem Set.weightEnumerator_eq_sum_monomial {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.weightEnumerator = ∑ w ∈ Finset.range (Fintype.card ι + 1), (MvPolynomial.monomial (Finsupp.single 0 (Fintype.card ι - w) + Finsupp.single 1 w)) ↑(C.weightDistribution w)

The monomial form of the weight enumerator.

@[simp]

theorem Set.coeff_weightEnumerator {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) (d : Fin 2 →₀ ℕ) : C.weightEnumerator.coeff d = if d 0 + d 1 = Fintype.card ι then ↑(C.weightDistribution (d 1)) else 0

The coefficients of the weight enumerator are the weight distribution: the coefficient of X^a Y^b is A_b(C) when a + b is the length, and zero otherwise.

theorem Set.isHomogeneous_weightEnumerator {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.weightEnumerator.IsHomogeneous (Fintype.card ι)

The weight enumerator is homogeneous of degree the length.

@[simp]

theorem Set.eval_one_weightEnumerator {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) : (MvPolynomial.eval 1) C.weightEnumerator = ↑(Nat.card ↑C)

The weight enumerator of a finite set of words evaluates to its cardinality at X = Y = 1.

The one-variable weight enumerator

noncomputable def Set.weightPolynomial {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : Polynomial ℤ

The one-variable weight enumerator ∑_w A_w(C) Y^w, the specialization of the homogeneous weight enumerator at X = 1.

theorem Set.weightPolynomial_def {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.weightPolynomial = ∑ w ∈ Finset.range (Fintype.card ι + 1), (Polynomial.monomial w) ↑(C.weightDistribution w)

@[simp]

theorem Set.coeff_weightPolynomial {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) (w : ℕ) : C.weightPolynomial.coeff w = ↑(C.weightDistribution w)

The coefficients of the one-variable weight enumerator are the weight distribution.

theorem Set.aeval_weightEnumerator {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : (MvPolynomial.aeval ![1, Polynomial.X]) C.weightEnumerator = C.weightPolynomial

The one-variable weight enumerator is the homogeneous one evaluated at X = 1.

@[simp]

theorem Set.eval_one_weightPolynomial {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} (hC : C.Finite) : Polynomial.eval 1 C.weightPolynomial = ↑(Nat.card ↑C)

The one-variable weight enumerator of a finite set of words evaluates to its cardinality at Y = 1.

theorem Set.natDegree_weightPolynomial_le {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (C : Set ((i : ι) → β i)) : C.weightPolynomial.natDegree ≤ Fintype.card ι

The one-variable weight enumerator has degree at most the length.

Recovering the minimum distance

theorem Set.hammingMinDist_eq_sInf_weightDistribution {ι : Type u_1} [Fintype ι] {β : ι → Type u_3} [(i : ι) → AddGroup (β i)] [(i : ι) → DecidableEq (β i)] {E : AddSubgroup ((i : ι) → β i)} (hE : (↑E).Finite) : (↑E).hammingMinDist = sInf {w : ℕ | 0 < w ∧ (↑E).weightDistribution w ≠ 0}

The minimum distance of a finite additive code is the least positive weight occurring in its weight distribution; both sides are zero for the zero code.

theorem TauCeti.weightDistribution_image {ι : Type u_1} {κ : Type u_2} {β : ι → Type u_3} {γ : κ → Type u_4} [Fintype ι] [Fintype κ] [(i : ι) → Zero (β i)] [(j : κ) → Zero (γ j)] [(i : ι) → DecidableEq (β i)] [(j : κ) → DecidableEq (γ j)] (C : Set ((i : ι) → β i)) (f : ((i : ι) → β i) ≃ ((j : κ) → γ j)) (hf : ∀ (x : (i : ι) → β i), hammingNorm (f x) = hammingNorm x) (w : ℕ) : (⇑f '' C).weightDistribution w = C.weightDistribution w

A weight-preserving equivalence preserves the weight distribution of any set of words.

theorem TauCeti.weightDistribution_eq_of_constant_weight {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {C : Set ((i : ι) → β i)} {d : ℕ} (hC : C.Finite) (h0 : 0 ∈ C) (hweight : ∀ x ∈ C, x ≠ 0 → hammingNorm x = d) (w : ℕ) : C.weightDistribution w = if w = 0 then 1 else if w = d then Nat.card ↑C - 1 else 0

A finite set containing zero whose nonzero words all have weight d has one word of weight zero and no words of any weight other than zero and d. For d ≠ 0 it has Nat.card C - 1 words of weight d. For d = 0 the set is the singleton {0}, whose one word has weight zero.

Elementary enumerators

@[simp]

theorem TauCeti.weightEnumerator_singleton {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) : {x}.weightEnumerator = MvPolynomial.X 0 ^ (Fintype.card ι - hammingNorm x) * MvPolynomial.X 1 ^ hammingNorm x

A singleton word has its weight monomial as weight enumerator.

theorem TauCeti.weightEnumerator_bot {ι : Type u_1} {R : Type u_2} [Fintype ι] [Semiring R] [DecidableEq R] : (↑⊥).weightEnumerator = MvPolynomial.X 0 ^ Fintype.card ι

The zero code has just its zero word, of weight zero.

@[simp]

theorem TauCeti.sum_ite_eq_zero_X_zero_X_one {R : Type u_2} [Zero R] [DecidableEq R] [Fintype R] : (∑ a : R, if a = 0 then MvPolynomial.X 0 else MvPolynomial.X 1) = MvPolynomial.X 0 + (↑(Nat.card R) - 1) * MvPolynomial.X 1

Summing the coordinate factor of a weight monomial, X at a zero letter and Y at a nonzero one, over an alphabet with q letters gives X + (q - 1) Y.

@[simp]

theorem TauCeti.weightEnumerator_univ {ι : Type u_1} {R : Type u_2} [Fintype ι] [Zero R] [DecidableEq R] [Finite R] : Set.univ.weightEnumerator = (MvPolynomial.X 0 + (↑(Nat.card R) - 1) * MvPolynomial.X 1) ^ Fintype.card ι

The whole word space has weight enumerator (X + (q - 1) Y)^n.

@[simp]

theorem TauCeti.aeval_weightEnumerator_diag {ι : Type u_1} {β : ι → Type u_2} [Fintype ι] [(i : ι) → Zero (β i)] [(i : ι) → DecidableEq (β i)] {R : Type u_3} [CommRing R] {C : Set ((i : ι) → β i)} (z : R) (hC : C.Finite) : (MvPolynomial.aeval ![z, z]) C.weightEnumerator = ↑(Nat.card ↑C) * z ^ Fintype.card ι

On the diagonal, the weight enumerator of a finite set of words is its cardinality times the common argument raised to the length.

Monomial equivalence and direct sums

theorem TauCeti.IsPermutationEquivalent.weightDistribution_eq {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq R] [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) (w : ℕ) : (↑C).weightDistribution w = (↑D).weightDistribution w

Permutation-equivalent codes have the same weight distribution.

theorem TauCeti.IsPermutationEquivalent.weightEnumerator_eq {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq R] [Semiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsPermutationEquivalent C D) : (↑C).weightEnumerator = (↑D).weightEnumerator

Permutation-equivalent codes have the same weight enumerator.

theorem TauCeti.IsMonomialEquivalent.weightDistribution_eq {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq R] [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) (w : ℕ) : (↑C).weightDistribution w = (↑D).weightDistribution w

Monomially equivalent codes have the same weight distribution.

theorem TauCeti.IsMonomialEquivalent.weightEnumerator_eq {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq R] [CommSemiring R] {C : Submodule R (ι → R)} {D : Submodule R (κ → R)} (h : IsMonomialEquivalent C D) : (↑C).weightEnumerator = (↑D).weightEnumerator

Monomially equivalent codes have the same weight enumerator.