Let \(G\) be a simple graph on a finite vertex type \(V\) with decidable adjacency, and write \(n = |V|\). The adjacency eigenvalues of \(G\) are the function

defined as the eigenvalues \(\lambda _0 \geq \lambda _1 \geq \cdots \geq \lambda _{n-1}\) of \(G.\operatorname {adjMatrix}(\mathbb {R})\), sorted in decreasing order. Concretely, this is (adjMatrix_isHermitian G).eigenvalues\(_0\).

Let \(G\) be a simple graph on a finite vertex type \(V\) with decidable adjacency, and suppose \(|V| \geq 2\). The second-largest eigenvalue \(\lambda _2\) of \(G\) is

i.e. the eigenvalue at index \(1\) in the decreasing sequence \(\lambda _0 \geq \lambda _1 \geq \cdots \).

Let \(G\) be a finite \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\). The spectral gap of \(G\) is

where \(\lambda _2(G)\) is the second-largest eigenvalue of \(G\). A larger spectral gap indicates better expansion properties.

Let \(\iota \) be an index type, \(n : \iota \to \mathbb {N}\) a family of sizes, \(s \in \mathbb {N}\) a uniform regularity degree, and \(G_i\) a simple \(s\)-regular graph on \(\operatorname {Fin}(n(i))\) for each \(i \in \iota \), with \(n(i) \geq 2\) for all \(i\). The family \(\{ G_i\} _{i \in \iota }\) is an expander family if there exists \(\varepsilon {\gt} 0\) such that

i.e. the spectral gap of every graph in the family is uniformly bounded below by \(\varepsilon \).

Let \(G\) be a finite \(s\)-regular simple graph on \(V\) with \(|V| \geq 2\). The graph \(G\) is Ramanujan if every eigenvalue \(\lambda \) of the adjacency matrix satisfying \(|\lambda | {\lt} s\) also satisfies

Formally, \(G\) is Ramanujan if for all \(i \in \operatorname {Fin}(|V|)\),

This is the optimal spectral bound for \(s\)-regular graphs.