Huang's induced subgraph theorem

Every set V of more than half of the points of the cube ι → Bool contains a point with at least √|ι| neighbors in V [Hua19]. More generally, for any set S of coordinates, some point of V has at least √|S| neighbors in V in the directions of S (BitString.exists_mem_sqrt_card_le_card_update_mem).

The theorem and its signed adjacency matrix, which squares to |ι|, are Huang's [Hua19]. Huang counts eigenvalues with Cauchy's interlacing theorem, which Mathlib lacks; here a dimension count replaces it. Mathlib's Archive/Sensitivity.lean formalizes the case S = univ, but the Archive cannot be imported.

Order the coordinates and sign the edge from x in direction i by the character of the coordinates of S below i. The resulting signed adjacency operator A along S (BitString.signedAdjacency) squares to |S| (BitString.signedAdjacency_signedAdjacency), because the two paths around every square of the cube carry opposite signs. So its eigenspaces for √|S| and -√|S| together span all functions on the cube, and one of them has dimension at least half the number of points. A function in that eigenspace vanishing outside V exists by counting dimensions; at a point where it is largest in absolute value, the eigenvalue equation compares √|S| times the largest value with a sum of at most as many values as there are neighbors in V.

Main definitions

• Cslib.BitString.signedAdjacency: the signed adjacency operator of the cube along a set of coordinates.

Main results

• Cslib.BitString.signedAdjacency_signedAdjacency: the signed adjacency operator along S squares to |S|.
• Cslib.BitString.exists_mem_sqrt_card_le_card_update_mem: Huang's induced subgraph theorem.

References

• H. Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture

def Cslib.BitString.signedAdjacency {ι : Type u_1} [LinearOrder ι] (S : Finset ι) : Module.End ℝ ((ι → Bool) → ℝ)

The signed adjacency operator of the cube along the coordinates of S: the value at x sums the values at the neighbors of x in the directions i ∈ S, the edge in direction i signed by the character of the coordinates of S below i.

theorem Cslib.BitString.signedAdjacency_apply {ι : Type u_1} [LinearOrder ι] (S : Finset ι) (v : (ι → Bool) → ℝ) (x : ι → Bool) : (signedAdjacency S) v x = ∑ i ∈ S, chi ℝ ({j ∈ S | j < i}) x * v (Function.update x i !x i)

theorem Cslib.BitString.signedAdjacency_signedAdjacency {ι : Type u_1} [LinearOrder ι] (S : Finset ι) (v : (ι → Bool) → ℝ) : (signedAdjacency S) ((signedAdjacency S) v) = ↑S.card • v

The signed adjacency operator squares to |S|: the diagonal terms each contribute the value at x, and the two paths around each square cancel.

theorem Cslib.BitString.exists_mem_sqrt_card_le_card_update_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] {V : Finset (ι → Bool)} (hV : 2 ^ Fintype.card ι < 2 * V.card) (S : Finset ι) : ∃ x ∈ V, √↑S.card ≤ ↑{i ∈ S | (Function.update x i !x i) ∈ V}.card

Huang's induced subgraph theorem: if V contains more than half of the points of the cube, then for every set S of coordinates some point of V has at least √|S| neighbors in V in the directions of S. For S = univ, the subgraph of the cube induced by V has maximum degree at least √|ι| [Hua19].