The expander mixing lemma and the Alon–Boppana bound
A Lean 4 / Mathlib formalization of two basic results of spectral graph theory, stated through the adjacency quadratic form on vectors orthogonal to the all-ones vector: the expander mixing lemma of Alon and Chung (for a d-regular graph on n ≥ 2 vertices with |x·Ax| ≤ μ‖x‖² on 𝟙⊥, |e(S,T) − d|S||T|/n| ≤ μ√(|S||T|)), and the Alon–Boppana bound in Nilli's form (a d-regular graph, d ≥ 2, with two vertices at distance at least 2k + 4 has a nonzero x ⟂ 𝟙 with x·Ax ≥ (2√(d−1) − (2√(d−1) − 1)/(k+1))‖x‖²). Mathlib has adjacency matrices but neither result.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000035
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000035/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000035/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'