# mathlib3documentation

mathlib-archive / sensitivity

# Huang's sensitivity theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A formalization of Hao Huang's sensitivity theorem: in the hypercube of dimension n ≥ 1, if one colors more than half the vertices then at least one vertex has at least √n colored neighbors.

A fun summer collaboration by Reid Barton, Johan Commelin, Jesse Han, Chris Hughes, Robert Y. Lewis, and Patrick Massot, based on Don Knuth's account of the story (https://www.cs.stanford.edu/~knuth/papers/huang.pdf), using the Lean theorem prover (https://leanprover.github.io/), by Leonardo de Moura at Microsoft Research, and his collaborators (https://leanprover.github.io/people/), and using Lean's user maintained mathematics library (https://github.com/leanprover-community/mathlib).

The project was developed at https://github.com/leanprover-community/lean-sensitivity and is now archived at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean

The next two lines assert we do not want to give a constructive proof, but rather use classical logic.

We also want to use the notation ∑ for sums.

### The hypercube #

Notations:

• ℕ denotes natural numbers (including zero).
• fin n = {0, ⋯ , n - 1}.
• bool = {tt, ff}.
@[protected, instance]
def sensitivity.Q.fintype (n : ) :
@[protected, instance]
def sensitivity.Q (n : ) :

The hypercube in dimension n.

Equations
Instances for sensitivity.Q
def sensitivity.π {n : } :

The projection from Q (n + 1) to Q n forgetting the first value (ie. the image of zero).

Equations

n will always denote a natural number.

@[protected, instance]

Q 0 has a unique element.

Equations
theorem sensitivity.Q.card (n : ) :
= 2 ^ n

Q n has 2^n elements.

Until the end of this namespace, n will be an implicit argument (still a natural number).

theorem sensitivity.Q.succ_n_eq {n : } (p q : sensitivity.Q (n + 1)) :
p = q p 0 = q 0

The adjacency relation defining the graph structure on Q n: p.adjacent q if there is an edge from p to q in Q n.

Equations

In Q 0, no two vertices are adjacent.

theorem sensitivity.Q.adj_iff_proj_eq {n : } {p q : sensitivity.Q (n + 1)} (h₀ : p 0 q 0) :

If p and q in Q (n+1) have different values at zero then they are adjacent iff their projections to Q n are equal.

theorem sensitivity.Q.adj_iff_proj_adj {n : } {p q : sensitivity.Q (n + 1)} (h₀ : p 0 = q 0) :

If p and q in Q (n+1) have the same value at zero then they are adjacent iff their projections to Q n are adjacent.

@[symm]
theorem sensitivity.Q.adjacent.symm {n : } {p q : sensitivity.Q n} :

### The vector space #

def sensitivity.V  :

The free vector space on vertices of a hypercube, defined inductively.

Equations
Instances for sensitivity.V

V n is a real vector space whose equality relation is computable.

@[protected, instance]
noncomputable def sensitivity.V.decidable_eq (n : ) :
Equations
@[protected, instance]
Equations
@[protected, instance]
def sensitivity.V.module (n : ) :
Equations
def sensitivity.e {n : } :

The basis of V indexed by the hypercube, defined inductively.

Equations
@[simp]
def sensitivity.ε {n : } (p : sensitivity.Q n) :

The dual basis to e, defined inductively.

Equations
theorem sensitivity.duality {n : } (p q : sensitivity.Q n) :
= ite (p = q) 1 0
theorem sensitivity.epsilon_total {n : } {v : sensitivity.V n} (h : (p : , v = 0) :
v = 0

Any vector in V n annihilated by all ε p's is zero.

e and ε are dual families of vectors. It implies that e is indeed a basis and ε computes coefficients of decompositions of vectors on that basis.

We will now derive the dimension of V, first as a cardinal in dim_V and, since this cardinal is finite, as a natural number in finrank_V

theorem sensitivity.dim_V {n : } :
= 2 ^ n
@[protected, instance]
theorem sensitivity.finrank_V {n : } :
= 2 ^ n

### The linear map #

def sensitivity.f (n : ) :

The linear operator $f_n$ corresponding to Huang's matrix $A_n$, defined inductively as a ℝ-linear map from V n to V n.

Equations

The preceding definition uses linear map constructions to automatically get that f is linear, but its values are somewhat buried as a side-effect. The next two lemmas unbury them.

@[simp]
theorem sensitivity.f_zero  :
theorem sensitivity.f_succ_apply {n : } (v : sensitivity.V (n + 1)) :
(sensitivity.f (n + 1)) v = ( v.fst + v.snd, v.fst - v.snd)

In the next statement, the explicit conversion (n : ℝ) of n to a real number is necessary since otherwise n • v refers to the multiplication defined using only the addition of V.

theorem sensitivity.f_squared {n : } (v : sensitivity.V n) :
( v) = n v

We now compute the matrix of f in the e basis (p is the line index, q the column index).

theorem sensitivity.f_matrix {n : } (p q : sensitivity.Q n) :
noncomputable def sensitivity.g (m : ) :

The linear operator $g_m$ corresponding to Knuth's matrix $B_m$.

Equations

In the following lemmas, m will denote a natural number.

Again we unpack what are the values of g.

theorem sensitivity.g_apply {m : } (v : sensitivity.V m) :
v = ( v + (m + 1) v, v)
theorem sensitivity.f_image_g {m : } (w : sensitivity.V (m + 1)) (hv : (v : , v = w) :
(sensitivity.f (m + 1)) w = (m + 1) w

### The main proof #

In this section, in order to enforce that n is positive, we write it as m + 1 for some natural number m.

dim X will denote the dimension of a subspace X as a cardinal.

fdim X will denote the (finite) dimension of a subspace X as a natural number.

Span S will denote the ℝ-subspace spanned by S.

Card X will denote the cardinal of a subset of a finite type, as a natural number.

In the following, ⊓ and ⊔ will denote intersection and sums of ℝ-subspaces, equipped with their subspace structures. The notations come from the general theory of lattices, with inf and sup (also known as meet and join).

theorem sensitivity.exists_eigenvalue {m : } (H : set (sensitivity.Q (m + 1))) (hH : H.to_finset.card 2 ^ m + 1) :
(y : sensitivity.V (m + 1)) (H : y , y 0

If a subset H of Q (m+1) has cardinal at least 2^m + 1 then the subspace of V (m+1) spanned by the corresponding basis vectors non-trivially intersects the range of g m.

theorem sensitivity.huang_degree_theorem {m : } (H : set (sensitivity.Q (m + 1))) (hH : H.to_finset.card 2 ^ m + 1) :
(q : sensitivity.Q (m + 1)), q H (m + 1) ((H q.adjacent).to_finset.card)

Huang sensitivity theorem also known as the Huang degree theorem