Grassmann graphs

AbbreviationVertices of the Grassmann graph#✓fully proved

For natural numbers \(k\) and \(\ell\), the vertices of the Grassmann graph \(\mathrm{Gr}(k, \ell)\) are the \(\ell\)-dimensional linear subspaces of \(\mathbb{F}_2^k\).

abbrev GrVertex (k ℓ : ℕ) : Type :=
  {L : Submodule 𝔽₂ (Fin k → 𝔽₂) // finrank 𝔽₂ L = ℓ}

Used by 3

Used byGrassmann graph over \(\mathbb{F}_2\) · Grassmann vertices between two subspaces · Non-expanding sets in the Grassmann graph (Khot–Minzer–Safra)

DefinitionGrassmann graph over \(\mathbb{F}_2\)#✓fully proved

For natural numbers \(k\) and \(\ell\), the Grassmann graph \(\mathrm{Gr}(k, \ell)\) has as vertices the \(\ell\)-dimensional linear subspaces of \(\mathbb{F}_2^k\), and two distinct such subspaces \(L\) and \(L'\) are adjacent when \(\dim(L \cap L') = \ell - 1\).

def Gr (k ℓ : ℕ) : SimpleGraph (GrVertex k ℓ) :=
  .fromRel (fun L L' ↦ finrank 𝔽₂ (L.val ⊓ L'.val :) = ℓ - 1)

Uses 1 · Used by 1

Statement usesVertices of the Grassmann graph

Used byNon-expanding sets in the Grassmann graph (Khot–Minzer–Safra)

DefinitionGrassmann vertices between two subspaces#✓fully proved

For natural numbers \(k\) and \(\ell\) and linear subspaces \(A\) and \(B\) of \(\mathbb{F}_2^k\), \(\mathrm{Gr}(k, \ell)[A, B]\) is the finite set of vertices \(L\) of the Grassmann graph \(\mathrm{Gr}(k, \ell)\), that is of \(\ell\)-dimensional subspaces of \(\mathbb{F}_2^k\), with \(A \subseteq L \subseteq B\). If \(A \not\subseteq B\) the set is empty.

This is the set \(\mathrm{Gr}_{k,\ell}[A, B]\) on page 13 of Khot, Minzer and Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion.

noncomputable def SubGr (k ℓ : ℕ) (A B : Submodule 𝔽₂ (Fin k → 𝔽₂)) : Finset (GrVertex k ℓ) :=
  {L | A ≤ L ∧ L ≤ B}

Uses 1 · Used by 1

Statement usesVertices of the Grassmann graph

Used byNon-expanding sets in the Grassmann graph (Khot–Minzer–Safra)

DefinitionEdge expansion of a vertex set#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\) and let \(S \subseteq V\) be nonempty. Let \(d\) be the degree in \(G\) of a fixed vertex of \(S\), chosen once for each \(S\). The expansion of \(S\) is the rational number \(\Phi_G(S) = |E(S, V \setminus S)| / (d \cdot |S|)\), where \(E(S, V \setminus S)\) is the set of edges of \(G\) with one endpoint in \(S\) and the other in \(V \setminus S\); it is \(0\) when \(d = 0\).

For a \(d\)-regular graph, \(d\) is the common degree and this is Definition 1.8 of Khot, Minzer and Safra, which also asks that \(|S| \le |V|/2\); neither regularity nor that bound is assumed here.

noncomputable def Φ {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
    (S : Finset V) (h : S.Nonempty) : ℚ :=
  #(G.interedges S Sᶜ) / (G.degree h.choose * #S)

Used by 1

Used byNon-expanding sets in the Grassmann graph (Khot–Minzer–Safra)

TheoremNon-expanding sets in the Grassmann graph (Khot–Minzer–Safra)#●ready to prove

For every real \(\alpha\) with \(0 < \alpha < 1\) there are a real \(\varepsilon > 0\) and a natural number \(r\) such that for all sufficiently large natural numbers \(\ell\) and, for each such \(\ell\), all sufficiently large natural numbers \(k\), the following holds. For subspaces \(A\) and \(B\) of \(\mathbb{F}_2^k\), let \(\mathrm{Gr}(k, \ell)[A, B]\) be the set of vertices \(L\) of the Grassmann graph \(\mathrm{Gr}(k, \ell)\) with \(A \subseteq L \subseteq B\). Let \(S\) be a nonempty set of at most half of the vertices of \(\mathrm{Gr}(k, \ell)\) whose edge expansion in \(\mathrm{Gr}(k, \ell)\) satisfies \(\Phi(S) \le \alpha\). Then there are subspaces \(A \subseteq B\) of \(\mathbb{F}_2^k\) such that the dimension of \(A\) plus the codimension \(k - \dim B\) of \(B\) is at most \(r\) and \(|S \cap \mathrm{Gr}(k, \ell)[A, B]| / |\mathrm{Gr}(k, \ell)[A, B]| \ge \varepsilon\).

public theorem_wanted theorem_1_12 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
    ∃ ε > 0, ∃ r, ∀ᶠ (ℓ : ℕ) (k : ℕ) in atTop, ∀ S : Finset (GrVertex k ℓ),
      (hS : S.Nonempty) → 2 * #S ≤ Fintype.card (GrVertex k ℓ) →
        Φ (Gr k ℓ) S hS ≤ α → ∃ (A B : Submodule 𝔽₂ (Fin k → 𝔽₂)), A ≤ B ∧
          letI a := finrank 𝔽₂ A; letI b := k - finrank 𝔽₂ B
          a + b ≤ r ∧ #(S ∩ SubGr k ℓ A B) / #(SubGr k ℓ A B) ≥ (ε : ℝ)

Sources

• S. Khot, D. Minzer, and M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Annals of Math, 198 (1) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_pseudorandom_grassmann of the lean-eval benchmark.

Uses 4

Statement usesGrassmann graph over \(\mathbb{F}_2\) · Vertices of the Grassmann graph · Grassmann vertices between two subspaces · Edge expansion of a vertex set

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.