Definition 14: Graph Expansion

Main Results

• adjMatrix_isHermitian: The adjacency matrix of a simple graph over ℝ is Hermitian.
• adjEigenvalues: The eigenvalues of the adjacency matrix, sorted in decreasing order.
• adjEigenvalues_antitone: The eigenvalues are sorted in decreasing order.
• secondLargestEigenvalue: The second-largest eigenvalue λ₂.
• spectralGap: The spectral gap s - λ₂.
• IsExpanderFamily: A family of s-regular graphs is expanding if the spectral gap is uniformly bounded below.
• IsRamanujan: A connected s-regular graph is Ramanujan if |λ| ≤ 2√(s-1) for all eigenvalues with |λ| < s.

Adjacency matrix is Hermitian

theorem GraphExpansion.adjMatrix_isHermitian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (SimpleGraph.adjMatrix ℝ G).IsHermitian

The adjacency matrix of a simple graph over ℝ is Hermitian. For real matrices, Hermitian is equivalent to symmetric, and the adjacency matrix is symmetric by SimpleGraph.isSymm_adjMatrix.

Eigenvalues of the adjacency matrix

noncomputable def GraphExpansion.adjEigenvalues {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Fin (Fintype.card V) → ℝ

The eigenvalues of the adjacency matrix G.adjMatrix ℝ, sorted in decreasing order and indexed by Fin (Fintype.card V).

Equations

• GraphExpansion.adjEigenvalues G = ⋯.eigenvalues₀

theorem GraphExpansion.adjEigenvalues_antitone {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Antitone (adjEigenvalues G)

The eigenvalues of the adjacency matrix are sorted in decreasing order (antitone): adjEigenvalues G i ≥ adjEigenvalues G j whenever i ≤ j.

Second-largest eigenvalue and spectral gap

noncomputable def GraphExpansion.secondLargestEigenvalue {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hcard : 2 ≤ Fintype.card V) : ℝ

The second-largest eigenvalue λ₂ of the adjacency matrix, defined when the graph has at least 2 vertices (2 ≤ Fintype.card V). This is adjEigenvalues G ⟨1, _⟩, the eigenvalue at index 1 in the decreasing sequence.

Equations

• GraphExpansion.secondLargestEigenvalue G hcard = GraphExpansion.adjEigenvalues G ⟨1, ⋯⟩

noncomputable def GraphExpansion.spectralGap {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hcard : 2 ≤ Fintype.card V) : ℝ

The spectral gap of a finite s-regular graph is (s : ℝ) - λ₂, where λ₂ is the second-largest eigenvalue of the adjacency matrix. A larger spectral gap indicates better expansion properties.

Equations

• GraphExpansion.spectralGap G s hcard = ↑s - GraphExpansion.secondLargestEigenvalue G hcard

Expander families

def GraphExpansion.IsExpanderFamily (ι : Type u_2) (n : ι → ℕ) (s : ℕ) (G : (i : ι) → SimpleGraph (Fin (n i))) [(i : ι) → DecidableRel (G i).Adj] (hcard : ∀ (i : ι), 2 ≤ Fintype.card (Fin (n i))) : Prop

A family of s-regular simple graphs {X_i}_{i : ι} is a family of expanders if there exists ε > 0 such that the second-largest eigenvalue satisfies λ₂(X_i) ≤ s - ε for all i. Equivalently, the spectral gap is uniformly bounded below by ε across the family. The vertex sets are Fin (n i) with varying sizes n : ι → ℕ, each having at least 2 vertices (ensured by hcard). The regularity degree s is uniform across the family.

Equations

• GraphExpansion.IsExpanderFamily ι n s G hcard = ∃ (ε : ℝ), 0 < ε ∧ ∀ (i : ι), GraphExpansion.secondLargestEigenvalue (G i) ⋯ ≤ ↑s - ε

Ramanujan graphs

noncomputable def GraphExpansion.IsRamanujan {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hcard : 2 ≤ Fintype.card V) : Prop

A finite s-regular graph is Ramanujan if the second-largest eigenvalue satisfies the optimal bound λ₂ ≤ 2√(s - 1). This is the best possible bound on λ₂ for s-regular graphs, achieved by Ramanujan graphs.

More precisely, a connected s-regular graph is Ramanujan if every eigenvalue λ of the adjacency matrix with |λ| < s satisfies |λ| ≤ 2√(s-1).

Equations

• GraphExpansion.IsRamanujan G s hcard = ∀ (i : Fin (Fintype.card V)), |GraphExpansion.adjEigenvalues G i| < ↑s → |GraphExpansion.adjEigenvalues G i| ≤ 2 * √(↑s - 1)