Volume of a Hamming ball: $|B(x,e)| = \sum_{i \le e} \binom{n}{i}(q-1)^i$

Open

EssentialCodingTheory.card_hammingBall

by chaikon · Oct 14, 2026 · Mathlib 0df444a (Lean v4.33.1)

coding-theorycombinatorics

Let $\alpha$ be a finite alphabet with $q = |\alpha|$ symbols, and let $n \ge 0$ . For a word $x \in \alpha^n$ and a radius $e \ge 0$ , the Hamming ball $B(x, e)$ is the set of words $y \in \alpha^n$ that differ from $x$ in at most $e$ coordinates. Its size is

|B(x, e)| = \sum_{i=0}^{e} \binom{n}{i} (q-1)^i.

The $i$ -th term counts the words at distance exactly $i$ from $x$ : choose the $i$ differing coordinates, then one of the $q - 1$ other symbols in each.

Preamble

import Mathlib.InformationTheory.Hamming
import Mathlib.Analysis.SpecialFunctions.Log.Base
open Finset

Formal statement

namespace EssentialCodingTheory
theorem card_hammingBall {α : Type*} [Fintype α] [DecidableEq α] {n : ℕ}
    (x : Fin n → α) (e : ℕ) :
    (univ.filter fun y : Fin n → α => hammingDist x y ≤ e).card =
      ∑ i ∈ range (e + 1), n.choose i * (Fintype.card α - 1) ^ i := by sorry
end EssentialCodingTheory

Source

V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory (web draft), https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf, §1.7, p. 21, equation (1.18) in the proof of Theorem 1.7.2; Hamming ball from Definition 1.6.1, p. 19.

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every finite type $\alpha$ with decidable equality, every natural number $n$ , every word $x \in \alpha^n$ , and every natural number $e$ :

\#\{\, y \in \alpha^n \;:\; d_H(x,y) \le e \,\} \;=\; \sum_{i=0}^{e} \binom{n}{i}\,(q \mathbin{\dot-} 1)^i .

The symbols mean the following:

$\alpha$ is any finite type (the alphabet). Equality on $\alpha$ is decidable. $q = |\alpha|$ is the number of elements of $\alpha$ .
$\alpha^n$ is the set of all functions $\{0,1,\dots,n-1\} \to \alpha$ , i.e. all length- $n$ words over $\alpha$ . $x$ is any fixed element of this set.
$d_H(x,y)$ is the Hamming distance: the number of coordinates $j \in \{0,\dots,n-1\}$ with $x_j \ne y_j$ .
The left side is the number of words $y \in \alpha^n$ (including $x$ itself) that differ from $x$ in at most $e$ coordinates. The inequality $\le e$ is non-strict.
The sum on the right runs over $i = 0, 1, \dots, e$ , which is $e+1$ terms. All arithmetic is in the natural numbers.
$\binom{n}{i}$ is the binomial coefficient. It equals $0$ when $i > n$ .
$q \mathbin{\dot-} 1$ is truncated subtraction: it equals $q-1$ when $q \ge 1$ and $0$ when $q = 0$ . Also $0^0 = 1$ .

Edge cases the statement includes:

$e \ge n$ : the terms with $i > n$ are zero. The right side is then $\sum_{i=0}^{n}\binom{n}{i}(q-1)^i$ , and the left side counts all of $\alpha^n$ .
$n = 0$ : $\alpha^0$ has exactly one element, the empty word. The left side is $1$ , and the right side is $\binom{0}{0}(q \mathbin{\dot-} 1)^0 = 1$ for every $e$ .
$e = 0$ : the right side is the single term $\binom{n}{0}(q \mathbin{\dot-} 1)^0 = 1$ .
$q = 1$ : the right side is $\binom{n}{0} \cdot 1 + \sum_{i \ge 1} \binom{n}{i}\cdot 0^i = 1$ .
$q = 0$ (empty $\alpha$ ) and $n \ge 1$ : no word $x$ exists, so the statement is vacuously true for these parameters.
$q = 0$ and $n = 0$ : this falls under the $n = 0$ case above.

The statement has no hypotheses beyond the finiteness of $\alpha$ and the decidability of equality on it. The preamble also imports a logarithm library, but the statement does not use it.

Human review

Endorsed by marwahaha · Oct 14, 2026
Endorsed by chaikon · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Volume of a Hamming ball: ∣B(x,e)∣=∑i≤e(ni)(q−1)i|B(x,e)| = \sum_{i \le e} \binom{n}{i}(q-1)^i∣B(x,e)∣=∑i≤e​(in​)(q−1)i

Volume of a Hamming ball: $|B(x,e)| = \sum_{i \le e} \binom{n}{i}(q-1)^i$