mathlib3 documentation

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 : ℕ) :

fintype (sensitivity.Q n)

@[protected, instance]

def sensitivity.Q.inhabited (n : ℕ) :

inhabited (sensitivity.Q n)

def sensitivity.Q (n : ℕ) :

The hypercube in dimension n.

Equations

sensitivity.Q n = (fin n → bool)

Instances for sensitivity.Q

def sensitivity.π {n : ℕ} :

sensitivity.Q (n + 1) → sensitivity.Q n

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

Equations

sensitivity.π = λ (p : sensitivity.Q (n + 1)), p ∘ fin.succ

n will always denote a natural number.

@[protected, instance]

def sensitivity.Q.unique :

unique (sensitivity.Q 0)

Q 0 has a unique element.

Equations

sensitivity.Q.unique = {to_inhabited := {default := λ (_x : fin 0), bool.tt}, uniq := sensitivity.Q.unique._proof_1}

theorem sensitivity.Q.card (n : ℕ) :

fintype.card (sensitivity.Q 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 ∧ sensitivity.π p = sensitivity.π q

def sensitivity.Q.adjacent {n : ℕ} (p : sensitivity.Q n) :

set (sensitivity.Q n)

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

p.adjacent = λ (q : sensitivity.Q n), ∃! (i : fin n), p i ≠ q i

theorem sensitivity.Q.not_adjacent_zero (p q : sensitivity.Q 0) :

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) :

p.adjacent q ↔ sensitivity.π p = sensitivity.π q

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) :

p.adjacent q ↔ (sensitivity.π p).adjacent (sensitivity.π q)

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} :

p.adjacent q ↔ q.adjacent p

The vector space #

def sensitivity.V :

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

Equations

sensitivity.V (n + 1) = (sensitivity.V n × sensitivity.V n)
sensitivity.V 0 = ℝ

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 : ℕ) :

decidable_eq (sensitivity.V n)

Equations

sensitivity.V.decidable_eq n = nat.rec (id (λ (a b : ℝ), a.decidable_eq b)) (λ (n_n : ℕ) (n_ih : decidable_eq (sensitivity.V n_n)), id (λ (a b : sensitivity.V n_n × sensitivity.V n_n), prod.lex.decidable_eq (sensitivity.V n_n) (sensitivity.V n_n) a b)) n

@[protected, instance]

def sensitivity.V.add_comm_group (n : ℕ) :

add_comm_group (sensitivity.V n)

Equations

sensitivity.V.add_comm_group n = nat.rec (id real.add_comm_group) (λ (n_n : ℕ) (n_ih : add_comm_group (sensitivity.V n_n)), id prod.add_comm_group) n

@[protected, instance]

def sensitivity.V.module (n : ℕ) :

module ℝ (sensitivity.V n)

Equations

sensitivity.V.module n = nat.rec (id real.module) (λ (n_n : ℕ) (n_ih : module ℝ (sensitivity.V n_n)), id prod.module) n

def sensitivity.e {n : ℕ} :

sensitivity.Q n → sensitivity.V n

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

Equations

sensitivity.e = λ (x : sensitivity.Q (n + 1)), cond (x 0) (sensitivity.e (sensitivity.π x), 0) (0, sensitivity.e (sensitivity.π x))
sensitivity.e = λ (_x : sensitivity.Q 0), 1

@[simp]

theorem sensitivity.e_zero_apply (x : sensitivity.Q 0) :

sensitivity.e x = 1

def sensitivity.ε {n : ℕ} (p : sensitivity.Q n) :

sensitivity.V n →ₗ[ℝ ] ℝ

The dual basis to e, defined inductively.

Equations

sensitivity.ε p = cond (p 0) ((sensitivity.ε (sensitivity.π p)).comp (linear_map.fst ℝ (sensitivity.V (n.add 0)) (sensitivity.V (n.add 0)))) ((sensitivity.ε (sensitivity.π p)).comp (linear_map.snd ℝ (sensitivity.V (n.add 0)) (sensitivity.V (n.add 0))))
sensitivity.ε _x = linear_map.id

theorem sensitivity.duality {n : ℕ} (p q : sensitivity.Q n) :

⇑(sensitivity.ε p) (sensitivity.e q) = ite (p = q) 1 0

theorem sensitivity.epsilon_total {n : ℕ} {v : sensitivity.V n} (h : ∀ (p : sensitivity.Q n), ⇑(sensitivity.ε p) v = 0) :

v = 0

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

def sensitivity.dual_bases_e_ε (n : ℕ) :

module.dual_bases sensitivity.e sensitivity.ε

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 : ℕ} :

module.rank ℝ (sensitivity.V n) = 2 ^ n

@[protected, instance]

def sensitivity.V.finite_dimensional {n : ℕ} :

finite_dimensional ℝ (sensitivity.V n)

theorem sensitivity.finrank_V {n : ℕ} :

fdim (sensitivity.V n) = 2 ^ n

The linear map #

def sensitivity.f (n : ℕ) :

sensitivity.V n →ₗ[ℝ ] sensitivity.V 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

sensitivity.f (n + 1) = ((sensitivity.f n).coprod linear_map.id).prod (linear_map.id.coprod (-sensitivity.f n))
sensitivity.f 0 = 0

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 :

sensitivity.f 0 = 0

theorem sensitivity.f_succ_apply {n : ℕ} (v : sensitivity.V (n + 1)) :

⇑(sensitivity.f (n + 1)) v = (⇑(sensitivity.f n) v.fst + v.snd, v.fst - ⇑(sensitivity.f n) 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) :

⇑(sensitivity.f n) (⇑(sensitivity.f 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) :

|⇑(sensitivity.ε q) (⇑(sensitivity.f n) (sensitivity.e p))| = ite (q.adjacent p) 1 0

noncomputable def sensitivity.g (m : ℕ) :

sensitivity.V m →ₗ[ℝ ] sensitivity.V (m + 1)

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

Equations

sensitivity.g m = (sensitivity.f m + √ (↑m + 1) • linear_map.id).prod linear_map.id

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) :

⇑(sensitivity.g m) v = (⇑(sensitivity.f m) v + √ (↑m + 1) • v, v)

theorem sensitivity.g_injective {m : ℕ} :

function.injective ⇑(sensitivity.g m)

theorem sensitivity.f_image_g {m : ℕ} (w : sensitivity.V (m + 1)) (hv : ∃ (v : sensitivity.V m), ⇑(sensitivity.g m) 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 ∈ Span (sensitivity.e '' H) ⊓ linear_map.range (sensitivity.g m)), 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