Theorem 5: Alon–Boppana Bound

Main Results

• alonBoppanaBound: For a finite, connected s-regular graph with s ≥ 3 and diameter D ≥ 2, we have λ₂ ≥ 2√(s-1) - (2√(s-1) - 1) / ⌊D/2⌋.
• alonBoppana_liminf: For any fixed s ≥ 3 and sequence of finite, connected s-regular graphs with |V| → ∞, liminf λ₂ ≥ 2√(s-1).

The proof uses Nilli's edge-based Laplacian approach (1991), constructing test vectors supported on edge-based layers and bounding the Rayleigh quotient.

Helper: diameter implies vertex count ≥ 2

theorem AlonBoppana.card_ge_two_of_diam_ge_two {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (hdiam : 2 ≤ G.diam) : 2 ≤ Fintype.card V

A graph with diameter ≥ 2 has at least 2 vertices.

theorem AlonBoppana.card_ge_two_of_regular {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 3 ≤ s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) : 2 ≤ Fintype.card V

A connected s-regular graph with s ≥ 3 has at least 2 vertices.

Courant–Fischer helper for second eigenvalue

theorem AlonBoppana.inner_apply_eq_sum_eigenvalues_mul_sq {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : Module.finrank ℝ E = n) {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (x : E) : inner ℝ (T x) x = ∑ i : Fin n, hT.eigenvalues hn i * inner ℝ ((hT.eigenvectorBasis hn) i) x ^ 2

Inner product ⟨Tx, x⟩ equals sum of eigenvalue-weighted squared coordinates for a symmetric operator. In a real inner product space with ONB of eigenvectors, ⟨Tx, x⟩ = Σ_i λ_i ⟨e_i, x⟩².

theorem AlonBoppana.rayleigh_le_second_eigenvalue {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : Module.finrank ℝ E = n) (hn2 : 2 ≤ n) {T : E →ₗ[ℝ] E} (hT : T.IsSymmetric) (x : E) (hx : x ≠ 0) (horth : inner ℝ ((hT.eigenvectorBasis hn) ⟨0, ⋯⟩) x = 0) : inner ℝ (T x) x ≤ hT.eigenvalues hn ⟨1, ⋯⟩ * ‖x‖ ^ 2

Courant–Fischer for second eigenvalue. For a symmetric operator with eigenvalues sorted decreasingly, if x ⊥ first eigenvector and x ≠ 0, the Rayleigh quotient ⟨Tx,x⟩/‖x‖² ≤ second eigenvalue.

Alon–Boppana Bound (Diameter-dependent form)

axiom AlonBoppana.alonBoppanaBound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 3 ≤ s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) (hdiam : 2 ≤ G.diam) : let hcard := ⋯; 2 * √(↑s - 1) - (2 * √(↑s - 1) - 1) / ↑⌊↑G.diam / 2⌋₊ ≤ GraphExpansion.secondLargestEigenvalue G hcard

Alon–Boppana Bound (quantitative form, Nilli 1991). For a finite, connected s-regular graph with s ≥ 3 and diameter D ≥ 2, the second-largest eigenvalue satisfies: λ₂ ≥ 2√(s-1) - (2√(s-1) - 1) / ⌊D/2⌋

theorem AlonBoppana.alonBoppanaBound_satisfiable : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (G : SimpleGraph V) (x_2 : DecidableRel G.Adj) (s : ℕ), 3 ≤ s ∧ G.Connected ∧ G.IsRegularOfDegree s ∧ 2 ≤ G.diam

Witness: the hypotheses of alonBoppanaBound are satisfiable. Demonstrated by K_{3,3}: 3-regular, connected, diameter 2.

Diameter grows with vertex count

For a connected s-regular graph, the number of vertices in a ball of radius r is at most 1 + s·((s-1)^r - 1)/(s-2). Hence n ≤ O((s-1)^{diam}), so diam ≥ Ω(log n).

theorem AlonBoppana.moore_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 3 ≤ s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) : ↑(Fintype.card V) * (↑s - 2) / ↑s ≤ (↑s - 1) ^ ↑G.diam

Moore bound: For a connected s-regular graph with s ≥ 3, card V * (s - 2) ≤ s * (s - 1) ^ diam. This follows from counting vertices in BFS layers from any vertex.

theorem AlonBoppana.diam_lower_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hs : 3 ≤ s) (hconn : G.Connected) (hreg : G.IsRegularOfDegree s) : Real.logb (↑s - 1) (↑(Fintype.card V) * (↑s - 2) / ↑s) ≤ ↑G.diam

A connected s-regular graph with s ≥ 3 and n vertices has diameter at least log_{s-1}(n · (s-2)/s).

theorem AlonBoppana.diam_lower_bound_satisfiable : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (G : SimpleGraph V) (x_2 : DecidableRel G.Adj) (s : ℕ), 3 ≤ s ∧ G.Connected ∧ G.IsRegularOfDegree s

Witness: diam_lower_bound is satisfiable (any connected s-regular graph with s ≥ 3 satisfies the hypotheses).

Asymptotic Alon–Boppana Bound

For fixed s ≥ 3, any sequence of connected s-regular graphs with vertex count tending to infinity satisfies liminf λ₂ ≥ 2√(s-1).

axiom AlonBoppana.alonBoppana_liminf (s : ℕ) (hs : 3 ≤ s) (n : ℕ → ℕ) (G : (i : ℕ) → SimpleGraph (Fin (n i))) [(i : ℕ) → DecidableRel (G i).Adj] (hconn : ∀ (i : ℕ), (G i).Connected) (hreg : ∀ (i : ℕ), (G i).IsRegularOfDegree s) (hcard : ∀ (i : ℕ), 2 ≤ Fintype.card (Fin (n i))) (htend : Filter.Tendsto n Filter.atTop Filter.atTop) : 2 * √(↑s - 1) ≤ Filter.liminf (fun (i : ℕ) => GraphExpansion.secondLargestEigenvalue (G i) ⋯) Filter.atTop

Asymptotic Alon–Boppana Bound. For a fixed degree s ≥ 3 and a sequence of finite, connected s-regular graphs whose vertex counts tend to infinity, the liminf of the second-largest eigenvalues is at least 2√(s-1).

This follows from alonBoppanaBound and diam_lower_bound:

• n i → ∞ implies diam(G_i) ≥ logb(s-1, n_i·(s-2)/s) → ∞ by the Moore bound
• For large i, diam(G_i) ≥ 2, so alonBoppanaBound gives λ₂(G_i) ≥ 2√(s-1) - (2√(s-1)-1)/⌊diam/2⌋
• As diam → ∞, the correction (2√(s-1)-1)/⌊diam/2⌋ → 0
• Taking liminf: liminf λ₂ ≥ 2√(s-1)

The proof requires connecting SimpleGraph.diam growth with Filter.liminf through logarithmic estimates and the Archimedean property, which needs infrastructure not directly available for SimpleGraph in Mathlib.

Eigenvalue bounds for regular graphs

theorem AlonBoppana.adjEigenvalue_abs_le {W : Type u_2} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (i : Fin (Fintype.card W)) : |GraphExpansion.adjEigenvalues G i| ≤ ↑s

All eigenvalues of the adjacency matrix of an s-regular graph lie in [-s, s]. Proved via the Gershgorin circle theorem: each eigenvalue lies in a disc of center A_{kk} = 0 and radius Σ_{j≠k} |A_{kj}| = degree(k) = s.

theorem AlonBoppana.adjEigenvalue_abs_le_satisfiable : ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (G : SimpleGraph W) (x_2 : DecidableRel G.Adj) (s : ℕ), G.IsRegularOfDegree s

Witness: adjEigenvalue_abs_le is satisfiable for any s-regular graph.

theorem AlonBoppana.secondLargestEigenvalue_ge_neg {W : Type u_2} [Fintype W] [DecidableEq W] (G : SimpleGraph W) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card W) : -↑s ≤ GraphExpansion.secondLargestEigenvalue G hcard

The second-largest eigenvalue of an s-regular graph is at least -(s : ℝ).

Corollary: Ramanujan bound is tight

theorem AlonBoppana.ramanujan_bound_optimal (s : ℕ) (hs : 3 ≤ s) (n : ℕ → ℕ) (G : (i : ℕ) → SimpleGraph (Fin (n i))) [(i : ℕ) → DecidableRel (G i).Adj] (hconn : ∀ (i : ℕ), (G i).Connected) (hreg : ∀ (i : ℕ), (G i).IsRegularOfDegree s) (hcard : ∀ (i : ℕ), 2 ≤ Fintype.card (Fin (n i))) (htend : Filter.Tendsto n Filter.atTop Filter.atTop) (ε : ℝ) (hε : 0 < ε) (hgap : ∀ (i : ℕ), GraphExpansion.secondLargestEigenvalue (G i) ⋯ ≤ ↑s - ε) : ε ≤ ↑s - 2 * √(↑s - 1)

The Ramanujan bound is tight. For any sequence of finite, connected s-regular graphs with vertex counts tending to infinity, and any uniform spectral gap ε > 0 (i.e., ∀ i, λ₂(G_i) ≤ s - ε), we must have ε ≤ s - 2√(s-1).

This follows from the asymptotic Alon–Boppana bound liminf λ₂ ≥ 2√(s-1): since each λ₂(G_i) ≤ s - ε, we get liminf λ₂ ≤ s - ε, and combining with 2√(s-1) ≤ liminf λ₂ yields ε ≤ s - 2√(s-1).

Hence the Ramanujan bound λ₂ ≤ 2√(s-1) is the best possible for expander families.