@[reducible, inline]

abbrev HarperIsoperimetric.HammingCube (n : ℕ) : Type

The Hamming cube $\{0,1\}^n$, modeled as functions Fin n → Bool.

def HarperIsoperimetric.hammingDist {n : ℕ} (x y : HammingCube n) : ℕ

Hamming distance between two points of $\{0,1\}^n$: number of coordinates at which they differ.

def HarperIsoperimetric.hammingBallFinset {n : ℕ} (c : HammingCube n) (r : ℕ) : Finset (HammingCube n)

The closed Hamming ball of radius $r$ centered at $c$: the set of points $x$ with $d_H(x, c) \leq r$.

def HarperIsoperimetric.IsHammingBall {n : ℕ} (B : Finset (HammingCube n)) : Prop

A subset $B$ of the Hamming cube is a Hamming ball if $B = B(c, r)$ for some center $c$ and radius $r$.

def HarperIsoperimetric.hammingExpansion {n : ℕ} (A : Finset (HammingCube n)) (t : ℕ) : Finset (HammingCube n)

The $t$-Hamming expansion of $A$: all points at Hamming distance at most $t$ from some element of $A$, i.e. $A_t = \{x : d_H(x, A) \leq t\}$.

theorem HarperIsoperimetric.harper_isoperimetric_inequality {n : ℕ} (A B : Finset (HammingCube n)) (hB : IsHammingBall B) (hcard : B.card ≤ A.card) (t : ℕ) (ht : 0 < t) : (hammingExpansion B t).card ≤ (hammingExpansion A t).card

Harper's isoperimetric inequality in the Hamming cube (Theorem 9.4.3, 1966): among all subsets of $\{0,1\}^n$ of a given cardinality, Hamming balls minimize the size of the $t$-expansion. Hence if $|B| \leq |A|$ and $B$ is a Hamming ball, then $|B_t| \leq |A_t|$.