def RapidExpansion.hammingWt {n : ℕ} (x : HarperIsoperimetric.HammingCube n) : ℕ

The Hamming weight of $x \in \{0, 1\}^n$, i.e. the number of coordinates equal to true; defined as the Hamming distance from the all-false vector.

def RapidExpansion.openHammingBall (n r : ℕ) : Finset (HarperIsoperimetric.HammingCube n)

The open Hamming ball of radius $r$ centred at the origin in $\{0, 1\}^n$: $\{x : \operatorname{wt}(x) < r\}$.

def RapidExpansion.bitFlip (n : ℕ) (x : HarperIsoperimetric.HammingCube n) : HarperIsoperimetric.HammingCube n

The bit-flip involution on the Hamming cube: $(\operatorname{flip}(x))_i = \neg x_i$ for every coordinate $i$.

theorem RapidExpansion.bitFlip_bitFlip (n : ℕ) (x : HarperIsoperimetric.HammingCube n) : bitFlip n (bitFlip n x) = x

The bit-flip map is an involution: $\operatorname{flip}(\operatorname{flip}(x)) = x$.

theorem RapidExpansion.hammingWt_bitFlip (n : ℕ) (x : HarperIsoperimetric.HammingCube n) : hammingWt (bitFlip n x) = n - hammingWt x

Flipping all bits complements the weight: $\operatorname{wt}(\operatorname{flip}(x)) = n - \operatorname{wt}(x)$.

theorem RapidExpansion.bitFlip_injective (n : ℕ) : Function.Injective (bitFlip n)

The bit-flip map is injective (in fact, a bijection, since it is its own inverse).

theorem RapidExpansion.card_openHammingBall_le (n : ℕ) : (openHammingBall n (n / 2)).card ≤ 2 ^ (n - 1)

The Hamming ball of radius $\lfloor n/2 \rfloor$ contains at most half of the cube: $|B(n, n/2)| \le 2^{n-1}$. The proof uses bit-flipping to inject the ball into its complement.

theorem RapidExpansion.openHammingBall_isHammingBall (n : ℕ) (hr : 0 < n / 2) : HarperIsoperimetric.IsHammingBall (openHammingBall n (n / 2))

The open Hamming ball of radius $n/2$ around the origin coincides with the closed Hamming ball of radius $n/2 - 1$, hence is a "Hamming ball" in the Harper sense.

theorem RapidExpansion.hammingExpansion_zero (n : ℕ) (S : Finset (HarperIsoperimetric.HammingCube n)) : HarperIsoperimetric.hammingExpansion S 0 = S

The $0$-expansion of a set is the set itself: $S_0 = S$.

theorem RapidExpansion.hammingExpansion_empty (n t : ℕ) : HarperIsoperimetric.hammingExpansion ∅ t = ∅

The $t$-expansion of the empty set is empty.

theorem RapidExpansion.harper_applied (n t : ℕ) (A : Finset (HarperIsoperimetric.HammingCube n)) (hA : 2 ^ (n - 1) ≤ A.card) : (HarperIsoperimetric.hammingExpansion (openHammingBall n (n / 2)) t).card ≤ (HarperIsoperimetric.hammingExpansion A t).card

Specialization of Harper's vertex-isoperimetric inequality: any $A \subseteq \{0, 1\}^n$ with $|A| \ge 2^{n-1}$ has $t$-expansion at least as large as that of the Hamming ball of radius $\lfloor n/2 \rfloor$.

theorem RapidExpansion.hammingWt_eq_filter_card {n : ℕ} (x : HarperIsoperimetric.HammingCube n) : hammingWt x = {i : Fin n | x i = true}.card

The Hamming weight equals the number of true coordinates: $\operatorname{wt}(x) = |\{i : x_i = \text{true}\}|$.

theorem RapidExpansion.hammingDist_self_eq_zero {n : ℕ} (x : HarperIsoperimetric.HammingCube n) : HarperIsoperimetric.hammingDist x x = 0

The Hamming distance from any point to itself is zero.

theorem RapidExpansion.hammingWt_le_add_dist {n : ℕ} (x y : HarperIsoperimetric.HammingCube n) : hammingWt x ≤ hammingWt y + HarperIsoperimetric.hammingDist x y

Triangle-style inequality for the Hamming weight: $\operatorname{wt}(x) \le \operatorname{wt}(y) + d(x, y)$.

theorem RapidExpansion.flip_dist_and_wt {n : ℕ} (x : HarperIsoperimetric.HammingCube n) (T : Finset (Fin n)) (hT : T ⊆ {i : Fin n | x i = true}) : have y := fun (i : Fin n) => if i ∈ T then false else x i; HarperIsoperimetric.hammingDist x y = T.card ∧ hammingWt y = hammingWt x - T.card

Flipping a subset $T$ of the $1$-coordinates of $x$ to $0$ produces a vector $y$ at Hamming distance $|T|$ from $x$ and of weight $\operatorname{wt}(x) - |T|$.

theorem RapidExpansion.expansion_openBall (n t : ℕ) (hn : 1 < n) : HarperIsoperimetric.hammingExpansion (openHammingBall n (n / 2)) t = openHammingBall n (n / 2 + t)

The $t$-expansion of the Hamming ball $B(n, n/2)$ is the Hamming ball $B(n, n/2 + t)$ of larger radius.

theorem RapidExpansion.chernoff_upper_tail_card (n t : ℕ) (hn : 0 < n) (ht : 0 < t) : ↑{x : HarperIsoperimetric.HammingCube n | n / 2 + t ≤ hammingWt x}.card < Real.exp (-2 * ↑t ^ 2 / ↑n) * 2 ^ n

Chernoff upper-tail bound for the cardinality of the heavy slice of the cube: the number of points $x \in \{0, 1\}^n$ with $\operatorname{wt}(x) \ge n/2 + t$ is strictly less than $e^{-2t^{2}/n} \cdot 2^{n}$.

theorem RapidExpansion.chernoff_hamming_ball (n t : ℕ) (hn : 0 < n) (ht : 0 < t) : (1 - Real.exp (-2 * ↑t ^ 2 / ↑n)) * 2 ^ n < ↑(openHammingBall n (n / 2 + t)).card

Chernoff-type lower bound on the size of the Hamming ball: $|B(n, n/2 + t)| > (1 - e^{-2t^{2}/n}) \cdot 2^{n}$.

theorem RapidExpansion.rapid_expansion_half_to_one_minus_eps (n : ℕ) (hn : 1 < n) (t : ℕ) (ht : 0 < t) (A : Finset (HarperIsoperimetric.HammingCube n)) (hA : 2 ^ (n - 1) ≤ A.card) : (1 - Real.exp (-2 * ↑t ^ 2 / ↑n)) * 2 ^ n < ↑(HarperIsoperimetric.hammingExpansion A t).card

Rapid expansion from half to $1 - \varepsilon$ (Theorem 9.4.5). For any $A \subseteq \{0, 1\}^n$ with $|A| \ge 2^{n-1}$ and any $t \ge 1$, the $t$-expansion satisfies $|A_t| > (1 - e^{-2t^{2}/n}) \cdot 2^{n}$.

theorem RapidExpansion.hammingDist_symm {n : ℕ} (x y : HarperIsoperimetric.HammingCube n) : HarperIsoperimetric.hammingDist x y = HarperIsoperimetric.hammingDist y x

Hamming distance is symmetric: $d(x, y) = d(y, x)$.

theorem RapidExpansion.hammingDist_triangle {n : ℕ} (x y z : HarperIsoperimetric.HammingCube n) : HarperIsoperimetric.hammingDist x z ≤ HarperIsoperimetric.hammingDist x y + HarperIsoperimetric.hammingDist y z

Triangle inequality for the Hamming distance: $d(x, z) \le d(x, y) + d(y, z)$.

theorem RapidExpansion.expansion_complement_disjoint_of_A {n : ℕ} (A : Finset (HarperIsoperimetric.HammingCube n)) (t : ℕ) : Disjoint (HarperIsoperimetric.hammingExpansion (Finset.univ \ HarperIsoperimetric.hammingExpansion A t) t) A

The $t$-expansion of the complement of $A_t$ is disjoint from $A$: any point reachable within distance $t$ from outside $A_t$ cannot lie in $A$ itself.

theorem RapidExpansion.expansion_expansion_subset {n : ℕ} (A : Finset (HarperIsoperimetric.HammingCube n)) (s t : ℕ) : HarperIsoperimetric.hammingExpansion (HarperIsoperimetric.hammingExpansion A s) t ⊆ HarperIsoperimetric.hammingExpansion A (s + t)

The iterated expansion is contained in a single larger expansion: $(A_s)_t \subseteq A_{s + t}$.

theorem RapidExpansion.card_univ_hammingCube (n : ℕ) : Finset.univ.card = 2 ^ n

The Hamming cube $\{0, 1\}^n$ has exactly $2^n$ elements.

theorem RapidExpansion.expansion_card_half (n : ℕ) (hn : 1 < n) (t : ℕ) (ht : 0 < t) (A : Finset (HarperIsoperimetric.HammingCube n)) (hA : Real.exp (-2 * ↑t ^ 2 / ↑n) * 2 ^ n ≤ ↑A.card) : 2 ^ (n - 1) ≤ (HarperIsoperimetric.hammingExpansion A t).card

Bootstrap lemma: if $|A| \ge e^{-2t^{2}/n} \cdot 2^{n}$, then the $t$-expansion of $A$ already has size at least $2^{n-1}$.

theorem RapidExpansion.rapid_expansion_eps_to_one_minus_eps (n : ℕ) (hn : 1 < n) (t : ℕ) (ht : 0 < t) (A : Finset (HarperIsoperimetric.HammingCube n)) (hA : Real.exp (-2 * ↑t ^ 2 / ↑n) * 2 ^ n ≤ ↑A.card) : (1 - Real.exp (-2 * ↑t ^ 2 / ↑n)) * 2 ^ n ≤ ↑(HarperIsoperimetric.hammingExpansion A (2 * t)).card

Rapid expansion from $\varepsilon$ to $1 - \varepsilon$ (Theorem 9.4.6). If $|A| \ge e^{-2t^{2}/n} \cdot 2^{n}$, then $|A_{2t}| \ge (1 - e^{-2t^{2}/n}) \cdot 2^{n}$.

theorem RapidExpansion.rapid_expansion_hamming (n : ℕ) (hn : 1 < n) (ε : ℝ) (hε : 0 < ε) (hε1 : ε < 1) (A : Finset (HarperIsoperimetric.HammingCube n)) (hA : ↑A.card ≥ ε * 2 ^ n) : have C := √(2 * Real.log (1 / ε)); ↑(HarperIsoperimetric.hammingExpansion A (2 * ⌈√(Real.log (1 / ε) * ↑n / 2)⌉₊)).card ≥ (1 - ε) * 2 ^ n

Rapid expansion in the Hamming cube (continuous form). If $|A| \ge \varepsilon \cdot 2^{n}$ for some $\varepsilon \in (0, 1)$, then for $t = \lceil \sqrt{\log(1/\varepsilon) \cdot n / 2} \rceil$, $|A_{2t}| \ge (1 - \varepsilon) \cdot 2^{n}$.