Skip to content

InformationTheory.Shannon.HypercubeEdge.Boundary

Imports 3

Boolean hypercube edge-boundary bound #

The edge boundary of a subset of the Boolean cube Fin n → Bool, defined combinatorially via directed coordinate-flip pairs, together with an edge-isoperimetric lower bound obtained from Loomis–Whitney and AM-GM.

Main definitions #

flipCoord i x — flip the i-th coordinate of x : Fin n → Bool, i.e. Function.update x i (!x i).
edgeBoundaryCount A — the number of pairs (x, i) with x ∈ A and flipCoord i x ∉ A, in bijection with the unordered edges of the cube having exactly one endpoint in A.
internalEdgePairCount A — the number of pairs (x, i) with x ∈ A and flipCoord i x ∈ A; it counts each unordered internal edge twice.

Main statements #

edge_total_count — edgeBoundaryCount A + internalEdgePairCount A = n * A.card.
internal_pair_count_eq_projection_sum — internalEdgePairCount A + 2 * ∑ i, (projectionExcept i A).card = 2 * (n * A.card).
edgeBoundary_count_eq — edgeBoundaryCount A + n * A.card = 2 * ∑ i, (projectionExcept i A).card.
sum_projection_card_ge_amgm — (n : ℝ) * (A.card)^((n-1)/n) ≤ ∑ i, ((projectionExcept i A).card : ℝ), from Loomis–Whitney and AM-GM.
edgeBoundary_ge_AMGM — for nonempty A, 2 * n * (A.card)^((n-1)/n) ≤ edgeBoundaryCount A + n * A.card, the additive form of |∂_e A| ≥ 2n · |A|^{(n-1)/n} − n · |A|.

Implementation notes #

The definitions avoid SimpleGraph and Sym2, working with naive combinatorial pairs to sidestep the SimpleGraph.edgeBoundary API. Counting identities are stated additively to avoid natural-number subtraction.

Coordinate flip and edge counts #

def

InformationTheory.Shannon.flipCoord

{n : ℕ} (i : Fin n) (x : Fin n → Bool) :

Fin n → Bool

Flip the i-th coordinate of x : Fin n → Bool.

Equations

InformationTheory.Shannon.flipCoord i x = Function.update x i !x i

Instances For

Used by

theorem

InformationTheory.Shannon.flipCoord_apply_same

@[simp]

{n : ℕ} (i : Fin n) (x : Fin n → Bool) :

flipCoord i x i = !x i

Used by

theorem

InformationTheory.Shannon.flipCoord_apply_other

{n : ℕ} (i : Fin n) (x : Fin n → Bool) {j : Fin n} (h : j ≠ i) :

flipCoord i x j = x j

Used by

theorem

InformationTheory.Shannon.flipCoord_flipCoord

@[simp]

{n : ℕ} (i : Fin n) (x : Fin n → Bool) :

flipCoord i (flipCoord i x) = x

Used by

def

InformationTheory.Shannon.edgeBoundaryCount

{n : ℕ} (A : Finset (Fin n → Bool)) :

The number of pairs (x, i) with x ∈ A and flipCoord i x ∉ A, in bijection with the cube edges having exactly one endpoint in A.

Equations

InformationTheory.Shannon.edgeBoundaryCount A = {p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ InformationTheory.Shannon.flipCoord p.2 p.1 ∉ A}.card

Instances For

Used by

def

InformationTheory.Shannon.internalEdgePairCount

{n : ℕ} (A : Finset (Fin n → Bool)) :

The number of pairs (x, i) with x ∈ A and flipCoord i x ∈ A, counting each internal edge twice.

Equations

InformationTheory.Shannon.internalEdgePairCount A = {p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ InformationTheory.Shannon.flipCoord p.2 p.1 ∈ A}.card

Instances For

Used by

Counting identities #

theorem

InformationTheory.Shannon.edge_total_count

{n : ℕ} (A : Finset (Fin n → Bool)) :

edgeBoundaryCount A + internalEdgePairCount A = n * A.card

The pairs (x, i) with x ∈ A number n * A.card, split disjointly by whether flipCoord i x ∈ A: edgeBoundaryCount A + internalEdgePairCount A = n * A.card.

Used by

Projection identity #

For each direction i, every fibre of projectionExcept i A is covered once or twice in A; double-counting these coverages relates ∑ i, (projectionExcept i A).card to A.card and the edge boundary count, stated additively to avoid natural-number subtraction.

theorem

InformationTheory.Shannon.flipCoord_mem_iff

{n : ℕ} (A : Finset (Fin n → Bool)) (x : Fin n → Bool) (i : Fin n) :

flipCoord i x ∈ A ↔ (Function.update x i !x i) ∈ A

flipCoord i x ∈ A ↔ Function.update x i (!x i) ∈ A, the definitional unfolding of flipCoord.

Used by

def

InformationTheory.Shannon.projMap

{n : ℕ} (i : Fin n) (x : Fin n → Bool) :

{ j : Fin n // j ≠ i } → Bool

The projection (Fin n → Bool) → ({j // j ≠ i} → Bool) dropping coordinate i.

Equations

InformationTheory.Shannon.projMap i x j = x ↑j

Instances For

Used by

def

InformationTheory.Shannon.extension

{n : ℕ} (i : Fin n) (b : Bool) (y : { j : Fin n // j ≠ i } → Bool) :

Fin n → Bool

Extend a projection by the bit b at coordinate i.

Equations

InformationTheory.Shannon.extension i b y j = if h : j = i then b else y ⟨j, h⟩

Instances For

Used by

theorem

InformationTheory.Shannon.extension_apply_eq

@[simp]

{n : ℕ} (i : Fin n) (b : Bool) (y : { j : Fin n // j ≠ i } → Bool) :

extension i b y i = b

Used by

theorem

InformationTheory.Shannon.extension_apply_ne

{n : ℕ} (i : Fin n) (b : Bool) (y : { j : Fin n // j ≠ i } → Bool) {j : Fin n} (h : j ≠ i) :

extension i b y j = y ⟨j, h⟩

Used by

theorem

InformationTheory.Shannon.projMap_extension

@[simp]

{n : ℕ} (i : Fin n) (b : Bool) (y : { j : Fin n // j ≠ i } → Bool) :

projMap i (extension i b y) = y

Used by

theorem

InformationTheory.Shannon.projectionExcept_eq_image

{n : ℕ} (i : Fin n) (A : Finset (Fin n → Bool)) :

projectionExcept i A = Finset.image (projMap i) A

Used by

theorem

InformationTheory.Shannon.extension_projMap_flip

{n : ℕ} (i : Fin n) (x : Fin n → Bool) :

extension i (!x i) (projMap i x) = flipCoord i x

flipCoord i x equals the extension of projMap i x by the flipped bit !x i.

Used by

theorem

InformationTheory.Shannon.projMap_eq_iff

{n : ℕ} (i : Fin n) (x : Fin n → Bool) (y : { j : Fin n // j ≠ i } → Bool) :

projMap i x = y ↔ x = extension i (x i) y

projMap i x = y ↔ x = extension i (x i) y.

Used by

def

InformationTheory.Shannon.boundaryDirSet

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) :

Finset (Fin n → Bool)

The boundary contribution in direction i: elements x ∈ A with flipCoord i x ∉ A.

Equations

InformationTheory.Shannon.boundaryDirSet A i = {x ∈ A | InformationTheory.Shannon.flipCoord i x ∉ A}

Instances For

Used by

theorem

InformationTheory.Shannon.fiber_projMap_eq_union

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) (y : { j : Fin n // j ≠ i } → Bool) :

{x ∈ A | projMap i x = y} = {x ∈ {extension i false y} | x ∈ A} ∪ {x ∈ {extension i true y} | x ∈ A}

Used by

theorem

InformationTheory.Shannon.boundaryDirSet_fiber_projMap_eq_union

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) (y : { j : Fin n // j ≠ i } → Bool) :

{x ∈ boundaryDirSet A i | projMap i x = y} = {x ∈ {extension i false y} | x ∈ A ∧ extension i true y ∉ A} ∪ {x ∈ {extension i true y} | x ∈ A ∧ extension i false y ∉ A}

Used by

theorem

InformationTheory.Shannon.extension_false_ne_extension_true

{n : ℕ} (i : Fin n) (y : { j : Fin n // j ≠ i } → Bool) :

extension i false y ≠ extension i true y

Used by

theorem

InformationTheory.Shannon.extension_mem_of_mem_projectionExcept

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) (y : { j : Fin n // j ≠ i } → Bool) (hy : y ∈ projectionExcept i A) :

extension i false y ∈ A ∨ extension i true y ∈ A

Used by

theorem

InformationTheory.Shannon.two_eq_fiber_card_add_boundaryDirSet_fiber_card

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) (y : { j : Fin n // j ≠ i } → Bool) (hy : y ∈ projectionExcept i A) :

2 = {x ∈ A | projMap i x = y}.card + {x ∈ boundaryDirSet A i | projMap i x = y}.card

Used by

theorem

InformationTheory.Shannon.boundaryPairCount_eq_boundaryDirSet_card

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) :

{p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ flipCoord p.2 p.1 ∉ A ∧ p.2 = i}.card = (boundaryDirSet A i).card

Used by

theorem

InformationTheory.Shannon.two_mul_projectionExcept_card_eq

{n : ℕ} (A : Finset (Fin n → Bool)) (i : Fin n) :

2 * (projectionExcept i A).card = A.card + {p : (Fin n → Bool) × Fin n | p.1 ∈ A ∧ flipCoord p.2 p.1 ∉ A ∧ p.2 = i}.card

Used by

theorem

InformationTheory.Shannon.two_sum_projection_eq

{n : ℕ} (A : Finset (Fin n → Bool)) :

2 * ∑ i : Fin n, (projectionExcept i A).card = n * A.card + edgeBoundaryCount A

2 * ∑ i, (projectionExcept i A).card = n * A.card + edgeBoundaryCount A, obtained by classifying each projection fibre as singly or doubly covered in A.

Used by

theorem

InformationTheory.Shannon.internal_pair_count_eq_projection_sum

{n : ℕ} (A : Finset (Fin n → Bool)) :

internalEdgePairCount A + 2 * ∑ i : Fin n, (projectionExcept i A).card = 2 * (n * A.card)

The internal edge pair count in projection-sum form: internalEdgePairCount A + 2 * ∑ i, (projectionExcept i A).card = 2 * (n * A.card).

Used by

theorem

InformationTheory.Shannon.edgeBoundary_count_eq

{n : ℕ} (A : Finset (Fin n → Bool)) :

edgeBoundaryCount A + n * A.card = 2 * ∑ i : Fin n, (projectionExcept i A).card

The edge boundary in projection-sum form: edgeBoundaryCount A + n * A.card = 2 * ∑ i, (projectionExcept i A).card.

Used by

Loomis–Whitney and AM-GM corollary #

theorem

InformationTheory.Shannon.sum_projection_card_ge_amgm

{n : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {A : Finset (Fin n → α)} (hA : A.Nonempty) :

↑n * (↑A.card ^ (n - 1)) ^ (↑n)⁻¹ ≤ ∑ i : Fin n, ↑(projectionExcept i A).card

(n : ℝ) * (A.card)^((n-1)/n) ≤ ∑ i, ((projectionExcept i A).card : ℝ), combining the Loomis–Whitney bound ∏ i, (projectionExcept i A).card ≥ A.card^(n-1) with AM-GM.

Used by

theorem

InformationTheory.Shannon.edgeBoundary_ge_AMGM

{n : ℕ} {A : Finset (Fin n → Bool)} (hA : A.Nonempty) :

2 * ↑n * (↑A.card ^ (n - 1)) ^ (↑n)⁻¹ ≤ ↑(edgeBoundaryCount A) + ↑n * ↑A.card

The edge-isoperimetric lower bound: for nonempty A ⊆ Fin n → Bool, 2 * n * (A.card)^((n-1)/n) ≤ edgeBoundaryCount A + n * A.card, the additive form of |∂_e A| ≥ 2n · |A|^{(n-1)/n} − n · |A|.

Used by