Harper's isoperimetric inequality

DefinitionHamming expansion#✓fully proved

Let \(\iota\) and \(F\) be finite, and view functions \(\iota \to F\) as words with the Hamming distance. For a finite set \(A\) of words and \(t \in \mathbb{N}\), the \(t\)-expansion of \(A\) is the set of words at Hamming distance at most \(t\) from some element of \(A\), that is, the union over \(a \in A\) of the closed Hamming balls of radius \(t\) about \(a\).

def expansion (A : Finset (ι → F)) (t : ℕ) : Finset (ι → F) :=
  A.biUnion fun a => ball a t

Uses 1 · Used by 1

Statement usesClosed Hamming ball

Used byHarper's isoperimetric inequality on the Hamming cube

DefinitionHamming ball predicate#✓fully proved

Let \(\iota\) and \(F\) be finite, and view functions \(\iota \to F\) as words with the Hamming distance. A set \(B\) of words is a Hamming ball if there are a word \(c\) and a radius \(e \in \mathbb{N}\) such that \(B\) is the closed Hamming ball of radius \(e\) about \(c\).

def IsBall (B : Finset (ι → F)) : Prop :=
  ∃ c : ι → F, ∃ e : ℕ, B = ball c e

Uses 1 · Used by 1

Statement usesClosed Hamming ball

Used byHarper's isoperimetric inequality on the Hamming cube

TheoremHarper's isoperimetric inequality on the Hamming cube#✓fully proved

Let \(n\) be a natural number. For points \(x, y \in \{0,1\}^n\), write \(d_H(x, y)\) for the Hamming distance between them, the number of coordinates in which they differ. For a set \(S \subseteq \{0,1\}^n\) and a natural number \(t\), write \(S_t\) for the set of points \(x \in \{0,1\}^n\) with \(d_H(x, s) \le t\) for some \(s \in S\). Let \(A\) and \(B\) be subsets of \(\{0,1\}^n\) such that \(B\) is a closed Hamming ball, that is, \(B = \{x : d_H(c, x) \le e\}\) for some \(c \in \{0,1\}^n\) and some natural number \(e\), and such that \(|B| \le |A|\). Then \(|B_t| \le |A_t|\) for every natural number \(t \ge 1\).

This is only the ball-comparison form of Harper's theorem: it does not assert that a ball exists at every cardinality and gives no equality cases.

theorem harper_isoperimetric_inequality
    {n : ℕ}
    (A B : Finset (Fin n → Bool))
    (hB : Hamming.IsBall B)
    (hcard : B.card ≤ A.card)
    (t : ℕ)
    (ht : 0 < t) :
    (Hamming.expansion B t).card ≤ (Hamming.expansion A t).card

Sources

• ATLAS ProbabilisticMethodsInCombinatorics, Theorem 9.4.3; the course text cites Harper without proof.
• L. H. Harper, "Optimal numberings and isoperimetric problems on graphs," Journal of Combinatorial Theory 1(3) (1966), 385–393, DOI 10.1016/S0021-9800(66)80059-5.

Uses 4

Statement usesHamming ball predicate · Hamming expansion

Proof usesClosed Hamming ball · Size of a Hamming ball

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.