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 #
n will always denote a natural number.
Until the end of this namespace,
n will be an implicit argument (still
a natural number).
The vector space #
The free vector space on vertices of a hypercube, defined inductively.
V n is a real vector space whose equality relation is computable.
The basis of
V indexed by the hypercube, defined inductively.
The dual basis to
e, defined inductively.
We will now derive the dimension of
V, first as a cardinal in
since this cardinal is finite, as a natural number in
The linear map #
The linear operator $f_n$ corresponding to Huang's matrix $A_n$,
defined inductively as a ℝ-linear map from
V n to
The preceding definition uses linear map constructions to automatically
f is linear, but its values are somewhat buried as a side-effect.
The next two lemmas unbury them.
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
We now compute the matrix of
f in the
e basis (
p is the line index,
q the column index).
In the following lemmas,
m will denote a natural number.
Again we unpack what are the values of
The main proof #
In this section, in order to enforce that
n is positive, we write it as
m + 1 for some natural number
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
Card X will denote the cardinal of a subset of a finite type, as a
In the following,
⊔ 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).
If a subset
Q (m+1) has cardinal at least
2^m + 1 then the
V (m+1) spanned by the corresponding basis vectors non-trivially
intersects the range of