Documentation

Archive.Sensitivity

Huang's sensitivity theorem #

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:

The hypercube in dimension n.

Equations
Instances For

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

    Equations
    Instances For
      theorem Sensitivity.Q.ext {n : } {f : Sensitivity.Q n} {g : Sensitivity.Q n} (h : ∀ (x : Fin n), f x = g x) :
      f = g

      n will always denote a natural number.

      Q n has 2^n elements.

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

      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
      Instances For

        In Q 0, no two vertices are adjacent.

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

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

        The vector space #

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

        Equations
        Instances For
          theorem Sensitivity.V.ext {n : } {p : Sensitivity.V (Nat.succ n)} {q : Sensitivity.V (Nat.succ n)} (h₁ : p.1 = q.1) (h₂ : p.2 = q.2) :
          p = q

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

          Equations
          Equations
          noncomputable def Sensitivity.e {n : } :

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

          Equations
          Instances For
            noncomputable def Sensitivity.ε {n : } :

            The dual basis to e, defined inductively.

            Equations
            • One or more equations did not get rendered due to their size.
            • Sensitivity.ε x_2 = LinearMap.id
            Instances For
              theorem Sensitivity.duality {n : } (p : Sensitivity.Q n) (q : Sensitivity.Q n) :
              (Sensitivity.ε p) (Sensitivity.e q) = if p = q then 1 else 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.

              theorem Sensitivity.dualBases_e_ε (n : ) :
              Module.DualBases 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

              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 V n.

              Equations
              Instances For

                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.

                theorem Sensitivity.f_succ_apply {n : } (v : Sensitivity.V (Nat.succ n)) :
                (Sensitivity.f (Nat.succ n)) v = ((Sensitivity.f n) v.1 + v.2, v.1 - (Sensitivity.f n) v.2)

                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.

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

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

                Equations
                Instances For

                  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 + Real.sqrt (m + 1) v, v)
                  theorem Sensitivity.f_image_g {m : } (w : Sensitivity.V (Nat.succ m)) (hv : ∃ (v : Sensitivity.V m), (Sensitivity.g m) v = w) :
                  (Sensitivity.f (Nat.succ m)) w = Real.sqrt (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 (Nat.succ m))) (hH : (Set.toFinset H).card 2 ^ m + 1) :
                  ∃ y ∈ Submodule.span (Sensitivity.e '' H) LinearMap.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 (Nat.succ m))) (hH : (Set.toFinset H).card 2 ^ m + 1) :
                  ∃ q ∈ H, Real.sqrt (m + 1) (Set.toFinset (H Sensitivity.Q.adjacent q)).card

                  Huang sensitivity theorem also known as the Huang degree theorem