Bounds on code size

TheoremSingleton bound#✓fully proved

Let \(\alpha\) be a nonempty finite alphabet with \(q\) letters, and let \(n\) and \(d\) be natural numbers with \(1 \le d \le n\). If \(C\) is a set of words of length \(n\) over \(\alpha\) in which any two distinct words are at Hamming distance at least \(d\), then \(C\) has at most \(q^{n - d + 1}\) elements.

The proof punctures the code to its first \(n - d + 1\) coordinates: two codewords agreeing on all retained coordinates can differ in at most the \(d - 1\) deleted coordinates, contradicting the minimum-distance hypothesis, so puncturing is injective on the code and the bound follows by counting the punctured words.

public theorem singleton_bound
    {α : Type*} [Fintype α] [DecidableEq α] [Nonempty α]
    {n d : ℕ}
    (C : Finset (Fin n → α))
    (hd1 : 1 ≤ d)
    (hd2 : d ≤ n)
    (hDist : ∀ c₁ ∈ C, ∀ c₂ ∈ C, c₁ ≠ c₂ →
      d ≤ hammingDist c₁ c₂) :
    C.card ≤ (Fintype.card α) ^ (n - d + 1)
Sources
  • R. C. Singleton, "Maximum distance q-nary codes", IEEE Transactions on Information Theory 10(2) (1964), 116–118, DOI 10.1109/TIT.1964.1053661.
Used by 1
Used bySingleton bound for linear codes, dimension form

DefinitionClosed Hamming ball#✓fully proved

For finite types \(\iota\) and \(F\), a word \(x : \iota \to F\) and a natural number \(e\), the closed Hamming ball of radius \(e\) about \(x\) is the finite set of all words \(y : \iota \to F\) whose Hamming distance from \(x\) is at most \(e\).

def ball (x : ι → F) (e : ℕ) : Finset (ι → F) :=
  Finset.univ.filter fun y => hammingDist x y ≤ e
Used by 6
Used byHamming expansion · Harper's isoperimetric inequality on the Hamming cube · Hamming ball predicate · Size of a Hamming ball · Size of a Hamming ball of fixed-length words · Hamming bound

TheoremSize of a Hamming ball#✓fully proved

For finite types \(\iota\) and \(F\), every word \(x : \iota \to F\) and every natural number \(e\), the closed Hamming ball of radius \(e\) about \(x\) has \(\sum_{k=0}^{e} \binom{|\iota|}{k} (|F| - 1)^k\) elements.

@[simp]
theorem card_ball (x : ι → F) (e : ℕ) :
    (ball x e).card =
      ∑ k ∈ Finset.range (e + 1),
        (Fintype.card ι).choose k * (Fintype.card F - 1) ^ k
Uses 1 · Used by 3
Statement usesClosed Hamming ball
Used byHarper's isoperimetric inequality on the Hamming cube · Size of a Hamming ball of fixed-length words · Hamming bound

TheoremSize of a Hamming ball of fixed-length words#✓fully proved

Let \(n \ge 1\) and let \(F\) be a finite alphabet with \(q \ge 2\) letters. For every word \(x \in F^n\) and every natural number \(e\), the closed Hamming ball of radius \(e\) about \(x\) has \(\sum_{k=0}^{e} \binom{n}{k} (q - 1)^k\) elements.

theorem card_ball_fin {n q : ℕ} (_hn : 0 < n) (hq : Fintype.card F = q) (_hq₂ : 2 ≤ q)
    (x : Fin n → F) (e : ℕ) :
    (ball x e).card = ∑ k ∈ Finset.range (e + 1), n.choose k * (q - 1) ^ k
Uses 2
Statement usesClosed Hamming ball
Proof usesSize of a Hamming ball

TheoremHamming bound#✓fully proved

Let \(\alpha\) be a finite alphabet with \(q \ge 2\) letters, and let \(n\) and \(t\) be natural numbers. If \(C\) is a set of words of length \(n\) over \(\alpha\) in which any two distinct words are at Hamming distance at least \(2t + 1\), then

\[|C| \sum_{i=0}^{t} \binom{n}{i} (q - 1)^i \le q^n.\]

The proof packs disjoint radius-\(t\) Hamming balls around the codewords into the ambient space: the distance hypothesis forces the balls apart (any overlap would give a triangle-inequality contradiction), and each ball contains exactly \(\sum_{i=0}^{t} \binom{n}{i} (q - 1)^i\) words.

This is the \(q\)-ary generalization of Hamming's binary sphere-packing bound. The original paper assumes binary words and derives the \(2^n\) form; the same disjoint-ball counting argument gives the formula stated here for an arbitrary finite alphabet.

Binary source: R. W. Hamming, "Error Detecting and Error Correcting Codes", Bell System Technical Journal 29 (1950), 147–160, DOI 10.1002/j.1538-7305.1950.tb00463.x.

public theorem hamming_sphere_packing_bound
    {α : Type*} [Fintype α] [DecidableEq α]
    {n t : ℕ}
    (C : Finset (Fin n → α))
    (hα : 2 ≤ Fintype.card α)
    (hDist : ∀ c₁ ∈ C, ∀ c₂ ∈ C, c₁ ≠ c₂ →
      2 * t + 1 ≤ hammingDist c₁ c₂) :
    C.card * (∑ i ∈ Finset.range (t + 1),
      n.choose i * (Fintype.card α - 1) ^ i) ≤ (Fintype.card α) ^ n
Uses 2 · Used by 1
Proof usesClosed Hamming ball · Size of a Hamming ball
Used byHamming bound for linear codes
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.