The Ramanujan bound 2√(k - 1)

The number 2√(k - 1) is the spectral radius of the k-regular infinite tree; a k-regular graph is Ramanujan when every adjacency eigenvalue λ has |λ| = k or |λ| ≤ 2√(k - 1). This file defines the bound and the predicate and proves elementary inequalities.

Main definitions

• SimpleGraph.bruhatTitsBound k: 2√(k - 1).
• SimpleGraph.IsRamanujan G k: G is k-regular and its eigenvalues satisfy the Ramanujan bound.

Main results

• SimpleGraph.bruhatTitsBound_le, SimpleGraph.bruhatTitsBound_lt: 2√(k - 1) ≤ k for k ≥ 1, strictly for k ≥ 3.
• SimpleGraph.bruhatTitsBound_mono: monotonicity in k.
• SimpleGraph.IsRamanujan.abs_eigenvalue_le: the eigenvalues of a Ramanujan graph satisfy |λ| ≤ k.

References

• A. Lubotzky, R. Phillips, P. Sarnak, Ramanujan graphs, Combinatorica 8 (1988) 261–277.

noncomputable def SimpleGraph.bruhatTitsBound (k : ℕ) : ℝ

The Bruhat-Tits spectral bound 2 · √(k − 1). For k = p + 1 prime, this is the spectral radius of the p + 1-regular infinite tree acting on ℓ² of its vertices.

Equations

• SimpleGraph.bruhatTitsBound k = 2 * √(↑k - 1)

@[simp]

theorem SimpleGraph.bruhatTitsBound_zero : bruhatTitsBound 0 = 0

@[simp]

theorem SimpleGraph.bruhatTitsBound_one : bruhatTitsBound 1 = 0

theorem SimpleGraph.bruhatTitsBound_nonneg (k : ℕ) : 0 ≤ bruhatTitsBound k

theorem SimpleGraph.bruhatTitsBound_le (k : ℕ) (hk : 1 ≤ k) : bruhatTitsBound k ≤ ↑k

Main theorem. For k ≥ 1, 2√(k−1) ≤ k. Equality holds iff k = 2. This is the algebraic content of why the Ramanujan bound is structurally meaningful: it is the strictest possible bound on non-trivial eigenvalues below the Frobenius eigenvalue k, achieved at k = 2, and otherwise strictly less than k.

theorem SimpleGraph.bruhatTitsBound_lt (k : ℕ) (hk : 3 ≤ k) : bruhatTitsBound k < ↑k

Strict bound. For k ≥ 3, 2√(k−1) < k. The strict-inequality companion to bruhatTitsBound_le. At k ∈ {0, 1, 2} equality (or trivial) holds, but from k = 3 onward there is a genuine spectral gap between the Frobenius eigenvalue k and the Ramanujan bound.

theorem SimpleGraph.bruhatTitsBound_sq (k : ℕ) (hk : 1 ≤ k) : bruhatTitsBound k ^ 2 = 4 * (↑k - 1)

Squared form. (2√(k−1))² = 4(k−1) for k ≥ 1. Useful for spectral arguments that compare bounds via second moments.

theorem SimpleGraph.bruhatTitsBound_mono {k k' : ℕ} (h : k ≤ k') : bruhatTitsBound k ≤ bruhatTitsBound k'

Monotonicity. The Bruhat-Tits bound is monotone in regularity.

def SimpleGraph.IsRamanujan {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : Prop

A k-regular SimpleGraph G is Ramanujan if every adjacency-matrix eigenvalue λ (over ℝ) satisfies |λ| = k (the trivial eigenvalues coming from k-regularity) or |λ| ≤ 2 · √(k − 1) (bounded by the Bruhat-Tits spectral bound).

The eigenvalue condition is stated using Module.End.HasEigenvalue on the linear endomorphism associated to the adjacency matrix.

Equations

• G.IsRamanujan k = (G.IsRegularOfDegree k ∧ ∀ (μ : ℝ), Module.End.HasEigenvalue (Matrix.toLin' (SimpleGraph.adjMatrix ℝ G)) μ → |μ| = ↑k ∨ |μ| ≤ SimpleGraph.bruhatTitsBound k)

theorem SimpleGraph.IsRamanujan.abs_eigenvalue_le {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {k : ℕ} (hk : 1 ≤ k) (hG : G.IsRamanujan k) {μ : ℝ} (hμ : Module.End.HasEigenvalue (Matrix.toLin' (adjMatrix ℝ G)) μ) : |μ| ≤ ↑k

Every adjacency-matrix eigenvalue of a k-regular Ramanujan graph satisfies the spectral bound |λ| ≤ k. This packages the Frobenius case and the Bruhat-Tits case into a single absolute-value bound.