Boolean cube basics

This file defines Boolean-cube vertices, Hamming distance, closed neighborhoods, simplicial order, initial segments, slicing maps, and the Harper boundary function H.

@[reducible, inline]

abbrev BooleanIsoperimetry.Cube (n : ℕ) : Type

A vertex of the n-dimensional Boolean cube, represented by its active coordinates.

Equations

• BooleanIsoperimetry.Cube n = Finset (Fin n)

noncomputable def BooleanIsoperimetry.hDist {n : ℕ} (x y : Cube n) : ℕ

The Hamming distance between two Boolean-cube vertices.

Equations

• BooleanIsoperimetry.hDist x y = Finset.card (symmDiff x y)

noncomputable def BooleanIsoperimetry.neighborhood {n : ℕ} (r : ℕ) (A : Finset (Cube n)) : Finset (Cube n)

The closed Hamming r-neighborhood of a family of cube vertices.

Equations

• BooleanIsoperimetry.neighborhood r A = {v : BooleanIsoperimetry.Cube n | ∃ u ∈ A, BooleanIsoperimetry.hDist u v ≤ r}

@[simp]

theorem BooleanIsoperimetry.mem_neighborhood_iff {n r : ℕ} {A : Finset (Cube n)} {v : Cube n} : v ∈ neighborhood r A ↔ ∃ u ∈ A, hDist u v ≤ r

noncomputable def BooleanIsoperimetry.hammingBall {n : ℕ} (r : ℕ) : Finset (Cube n)

The closed Hamming ball of radius r centered at the origin.

Equations

• BooleanIsoperimetry.hammingBall r = {v : BooleanIsoperimetry.Cube n | Finset.card v ≤ r}

noncomputable def BooleanIsoperimetry.cubeToNat {n : ℕ} (x : Cube n) : ℕ

The binary encoding used to break ties in the simplicial order.

Equations

• BooleanIsoperimetry.cubeToNat x = ∑ i ∈ x, 2 ^ ↑i

def BooleanIsoperimetry.simplicialLe {n : ℕ} (x y : Cube n) : Prop

The non-strict simplicial order: first by weight, then by reverse binary order.

Equations

• BooleanIsoperimetry.simplicialLe x y = (Finset.card x < Finset.card y ∨ Finset.card x = Finset.card y ∧ BooleanIsoperimetry.cubeToNat y ≤ BooleanIsoperimetry.cubeToNat x)

def BooleanIsoperimetry.simplicialLt {n : ℕ} (x y : Cube n) : Prop

The strict simplicial order on Boolean-cube vertices.

Equations

• BooleanIsoperimetry.simplicialLt x y = (BooleanIsoperimetry.simplicialLe x y ∧ ¬BooleanIsoperimetry.simplicialLe y x)

theorem BooleanIsoperimetry.sum_pow_two_lt (n : ℕ) : ∑ i ∈ Finset.range n, 2 ^ i < 2 ^ n

theorem BooleanIsoperimetry.cubeToNat_inj {n : ℕ} {x y : Cube n} (h : cubeToNat x = cubeToNat y) : x = y

theorem BooleanIsoperimetry.simplicialLe_refl {n : ℕ} (a : Cube n) : simplicialLe a a

theorem BooleanIsoperimetry.simplicialLe_trans {n : ℕ} (a b c : Cube n) (hab : simplicialLe a b) (hbc : simplicialLe b c) : simplicialLe a c

theorem BooleanIsoperimetry.simplicialLe_antisymm {n : ℕ} (a b : Cube n) (hab : simplicialLe a b) (hba : simplicialLe b a) : a = b

theorem BooleanIsoperimetry.simplicialLe_total {n : ℕ} (a b : Cube n) : simplicialLe a b ∨ simplicialLe b a

noncomputable def BooleanIsoperimetry.rank {n : ℕ} (x : Cube n) : ℕ

The zero-based position of a vertex in the simplicial order.

Equations

• BooleanIsoperimetry.rank x = {y : BooleanIsoperimetry.Cube n | BooleanIsoperimetry.simplicialLt y x}.card

noncomputable def BooleanIsoperimetry.simplicialInitSeg (n k : ℕ) : Finset (Cube n)

The first k vertices of the n-cube in simplicial order.

Equations

• BooleanIsoperimetry.simplicialInitSeg n k = {x : BooleanIsoperimetry.Cube n | BooleanIsoperimetry.rank x < k}

theorem BooleanIsoperimetry.rank_lt_two_pow {n : ℕ} (x : Cube n) : rank x < 2 ^ n

theorem BooleanIsoperimetry.rank_strictMono {n : ℕ} {x y : Cube n} (h : simplicialLt x y) : rank x < rank y

theorem BooleanIsoperimetry.rank_lt_of_mem_simplicialInitSeg {n k : ℕ} {x : Cube n} (hx : x ∈ simplicialInitSeg n k) : rank x < k

theorem BooleanIsoperimetry.rank_injective {n : ℕ} : Function.Injective rank

theorem BooleanIsoperimetry.rank_image_eq {n : ℕ} : Finset.image rank Finset.univ = Finset.range (2 ^ n)

theorem BooleanIsoperimetry.card_simplicialInitSeg {n k : ℕ} : (simplicialInitSeg n k).card = min k (2 ^ n)

noncomputable def BooleanIsoperimetry.embed0 {n : ℕ} (x : Cube n) : Cube (n + 1)

Embed an n-cube vertex in dimension n + 1 with last coordinate zero.

Equations

• BooleanIsoperimetry.embed0 x = Finset.image Fin.castSucc x

noncomputable def BooleanIsoperimetry.embed1 {n : ℕ} (x : Cube n) : Cube (n + 1)

Embed an n-cube vertex in dimension n + 1 with last coordinate one.

Equations

• BooleanIsoperimetry.embed1 x = insert (Fin.last n) (Finset.image Fin.castSucc x)

noncomputable def BooleanIsoperimetry.slice0 {n : ℕ} (A : Finset (Cube (n + 1))) : Finset (Cube n)

The lower slice of a family in dimension n + 1.

Equations

• BooleanIsoperimetry.slice0 A = {x : BooleanIsoperimetry.Cube n | BooleanIsoperimetry.embed0 x ∈ A}

noncomputable def BooleanIsoperimetry.slice1 {n : ℕ} (A : Finset (Cube (n + 1))) : Finset (Cube n)

The upper slice of a family in dimension n + 1.

Equations

• BooleanIsoperimetry.slice1 A = {x : BooleanIsoperimetry.Cube n | BooleanIsoperimetry.embed1 x ∈ A}

theorem BooleanIsoperimetry.slice_card_add {n : ℕ} (A : Finset (Cube (n + 1))) : (slice0 A).card + (slice1 A).card = A.card

theorem BooleanIsoperimetry.hDist_embed0_embed0 {n : ℕ} (x y : Cube n) : hDist (embed0 x) (embed0 y) = hDist x y

theorem BooleanIsoperimetry.hDist_embed1_embed1 {n : ℕ} (x y : Cube n) : hDist (embed1 x) (embed1 y) = hDist x y

theorem BooleanIsoperimetry.hDist_embed0_embed1 {n : ℕ} (x y : Cube n) : hDist (embed0 x) (embed1 y) = hDist x y + 1

theorem BooleanIsoperimetry.slice0_neighborhood {n : ℕ} (A : Finset (Cube (n + 1))) : slice0 (neighborhood 1 A) = neighborhood 1 (slice0 A) ∪ slice1 A

theorem BooleanIsoperimetry.slice1_neighborhood {n : ℕ} (A : Finset (Cube (n + 1))) : slice1 (neighborhood 1 A) = neighborhood 1 (slice1 A) ∪ slice0 A

theorem BooleanIsoperimetry.neighborhood_succ {n : ℕ} (A : Finset (Cube (n + 1))) : (neighborhood 1 A).card = (neighborhood 1 (slice0 A) ∪ slice1 A).card + (neighborhood 1 (slice1 A) ∪ slice0 A).card

noncomputable def BooleanIsoperimetry.H (n k : ℕ) : ℕ

The size of the radius-one neighborhood of the simplicial initial segment of size k.

Equations

• BooleanIsoperimetry.H n k = (BooleanIsoperimetry.neighborhood 1 (BooleanIsoperimetry.simplicialInitSeg n k)).card

theorem BooleanIsoperimetry.H_zero (n : ℕ) : H n 0 = 0

theorem BooleanIsoperimetry.H_mono {n a b : ℕ} (h : a ≤ b) : H n a ≤ H n b

theorem BooleanIsoperimetry.H_le_cube (n k : ℕ) : H n k ≤ 2 ^ n

theorem BooleanIsoperimetry.H_ge_self (n k : ℕ) (hk : k ≤ 2 ^ n) : k ≤ H n k

theorem BooleanIsoperimetry.H_full (n : ℕ) : H n (2 ^ n) = 2 ^ n

theorem BooleanIsoperimetry.initSeg_nested {n k m : ℕ} (h : k ≤ m) : simplicialInitSeg n k ⊆ simplicialInitSeg n m

theorem BooleanIsoperimetry.card_initSeg_union {n a b : ℕ} (ha : a ≤ 2 ^ n) (hb : b ≤ 2 ^ n) : (simplicialInitSeg n a ∪ simplicialInitSeg n b).card = max a b

theorem BooleanIsoperimetry.rank_mono {n : ℕ} {a b : Cube n} (h : simplicialLe a b) : rank a ≤ rank b

noncomputable def BooleanIsoperimetry.gShift {n : ℕ} (v : Cube n) : Cube n

Remove the least active coordinate, giving the lowest-rank vertex in the closed unit ball.

Equations

• BooleanIsoperimetry.gShift v = if h : Finset.Nonempty v then Finset.erase v (Finset.min' v h) else v

theorem BooleanIsoperimetry.hDist_gShift_le {n : ℕ} (v : Cube n) : hDist (gShift v) v ≤ 1

theorem BooleanIsoperimetry.gShift_le_ball {n : ℕ} {u v : Cube n} (h : hDist u v ≤ 1) : simplicialLe (gShift v) u

theorem BooleanIsoperimetry.mem_neighborhood_initSeg_iff {n k : ℕ} {v : Cube n} : v ∈ neighborhood 1 (simplicialInitSeg n k) ↔ rank (gShift v) < k

theorem BooleanIsoperimetry.card_gShift {n : ℕ} (v : Cube n) : Finset.card (gShift v) = Finset.card v - 1

theorem BooleanIsoperimetry.cubeToNat_erase {n : ℕ} {x : Cube n} {a : Fin n} (ha : a ∈ x) : cubeToNat x = cubeToNat (Finset.erase x a) + 2 ^ ↑a

theorem BooleanIsoperimetry.cubeToNat_lt_two_pow {n M : ℕ} {x : Cube n} (h : ∀ i ∈ x, ↑i < M) : cubeToNat x < 2 ^ M

theorem BooleanIsoperimetry.cubeToNat_gShift_le {n : ℕ} (x : Cube n) : cubeToNat (gShift x) ≤ cubeToNat x

theorem BooleanIsoperimetry.cubeToNat_gShift_erase_max {n : ℕ} {x : Cube n} (hx : Finset.Nonempty x) (h2 : 2 ≤ Finset.card x) : cubeToNat (gShift x) = cubeToNat (gShift (Finset.erase x (Finset.max' x hx))) + 2 ^ ↑(Finset.max' x hx)

theorem BooleanIsoperimetry.cubeToNat_gShift_mono {n : ℕ} (m : ℕ) (s t : Cube n) : Finset.card s = m → Finset.card t = m → cubeToNat t ≤ cubeToNat s → cubeToNat (gShift t) ≤ cubeToNat (gShift s)

theorem BooleanIsoperimetry.gShift_monotone {n : ℕ} {w v : Cube n} (h : simplicialLe w v) : simplicialLe (gShift w) (gShift v)

theorem BooleanIsoperimetry.downwardClosed_eq_initSeg {n : ℕ} {S : Finset (Cube n)} (hS : ∀ (x y : Cube n), simplicialLe x y → y ∈ S → x ∈ S) : S = simplicialInitSeg n S.card

theorem BooleanIsoperimetry.neighborhood_initSeg_eq {n k : ℕ} : neighborhood 1 (simplicialInitSeg n k) = simplicialInitSeg n (H n k)

theorem BooleanIsoperimetry.embed0_card {n : ℕ} (x : Cube n) : Finset.card (embed0 x) = Finset.card x

theorem BooleanIsoperimetry.embed0_cubeToNat {n : ℕ} (x : Cube n) : cubeToNat (embed0 x) = cubeToNat x

theorem BooleanIsoperimetry.embed1_card {n : ℕ} (x : Cube n) : Finset.card (embed1 x) = Finset.card x + 1

theorem BooleanIsoperimetry.embed1_cubeToNat {n : ℕ} (x : Cube n) : cubeToNat (embed1 x) = cubeToNat x + 2 ^ n

theorem BooleanIsoperimetry.embed0_mono {n : ℕ} {x y : Cube n} (h : simplicialLe x y) : simplicialLe (embed0 x) (embed0 y)

theorem BooleanIsoperimetry.embed1_mono {n : ℕ} {x y : Cube n} (h : simplicialLe x y) : simplicialLe (embed1 x) (embed1 y)

theorem BooleanIsoperimetry.slice0_initSeg_eq {n k : ℕ} : slice0 (simplicialInitSeg (n + 1) k) = simplicialInitSeg n (slice0 (simplicialInitSeg (n + 1) k)).card

theorem BooleanIsoperimetry.slice1_initSeg_eq {n k : ℕ} : slice1 (simplicialInitSeg (n + 1) k) = simplicialInitSeg n (slice1 (simplicialInitSeg (n + 1) k)).card

theorem BooleanIsoperimetry.H_succ_slice {n k : ℕ} : H (n + 1) k = max (H n (slice0 (simplicialInitSeg (n + 1) k)).card) (slice1 (simplicialInitSeg (n + 1) k)).card + max (H n (slice1 (simplicialInitSeg (n + 1) k)).card) (slice0 (simplicialInitSeg (n + 1) k)).card

def BooleanIsoperimetry.binomPrefix (n r : ℕ) : ℕ

The sum of the first r binomial coefficients in row n.

Equations

• BooleanIsoperimetry.binomPrefix n r = ∑ i ∈ Finset.range r, n.choose i

def BooleanIsoperimetry.choosePred (n r : ℕ) : ℕ

The binomial coefficient immediately preceding layer r, with value zero at r = 0.

Equations

• BooleanIsoperimetry.choosePred n r = if r = 0 then 0 else n.choose (r - 1)