1 Spectral theory of regular graphs

In this chapter, we introduce the definitions related to regular graphs and their spectrum. We refer the reader to [ for a more detailed introduction and motivations.

As in Graph, a graph is a pair \(G = (V, E)\) where \(V\) is a set of vertices, and \(E\) a set of edges, and each edge links two unordered, possibly identical vertices. The notations \(V(G)\) and \(E(G)\) respectively denote the subsets of \(V\) and \(E\) corresponding to vertices or edges of \(G\).

Note that this definition allows for loops (i.e. edges going from one vertex to itself) and multi-edges (i.e. multiple edges connecting two vertices). This convention is essential to the proof we are aiming for, which is why we use Graph instead of the more developed SimpleGraph.

Following Inc, we say an edge \(e\) is incident to a vertex \(x\) if there exists a vertex \(y\) such that \(e\) links \(x\) and \(y\). As IsLoopAt, an edge is a loop based at a vertex \(x\) if it links the vertex \(x\) to itself.

1.1 Basic notions of graph theory

Let us define a few basic notions from graph theory. We make definitions with minimal hypotheses as these are fundamental objects that should be added to Mathlib.

1.1.1 General definitions

Definition 1

We say a graph \(G\) is empty if \(V(G) = \emptyset \).

Definition 2

A graph \(G\) is bipartite if there exists two disjoint subsets \(U_1\), \(U_2\) of \(V(G)\) such that, for all \(e \in E(G)\), \(e\) links an element of \(U_1\) and an element of \(U_2\).

1.1.2 Paths and distance

We define a notion of walk on the graph, and a corresponding distance function. Let \(G\) be a graph.

Definition 3

Let \(x, y \in V(G)\). A walk from \(x\) to \(y\) on \(G\) is given by:

a non-negative integer \(m\);
an ordered sequence of \(m+1\) vertices \(v_0, \ldots , v_m \in V(G)\);
an ordered sequence of \(m\) edges \(e_1, \ldots , e_m \in E(G)\);

satisfying the following:

\(v_0=x\) and \(v_m=y\);
for any \(i \in \{ 1, \ldots , m\} \), \(e_i\) links \(v_{i-1}\) and \(v_i\).

The integer \(m\) is the length of the walk.

Definition 4

We say \(G\) is connected if, for all \(x\), \(y \in V(G)\), there exists a walk from \(x\) to \(y\).

Definition 5

todo

Definition 6

todo

Definition 7

todo

1.1.3 Notions of finiteness

Let \(G\) be a graph.

Definition 8

Let \(x\) be a vertex of \(G\). We say \(G\) is locally finite at \(x\) if \(\mathrm{incidenceSet}(x)\) is finite.

Definition 9

\(G\) is said to be locally finite if, for all \(x \in V(G)\), \(G\) is locally finite at \(x\).

Definition 10

We say \(G\) is finite if \(V(G)\) and \(E(G)\) are both finite.

Proposition 11

\(G\) is finite if and only if \(V(G)\) is finite and \(G\) is locally finite.

1.1.4 Degree and regularity

Let \(G\) be a graph.

Definition 12

Let \(x\) be a vertex of \(G\). We assume \(G\) is locally finite at \(x\). The degree of \(x\) is the number of incident edges, counting loops twice:

\begin{equation*} \mathrm{deg}(x) = \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)}. \end{equation*}

Definition 13

Let \(d\) be a non-negative integer. We say \(G\) is regular of degree \(d\) if it is not empty, locally finite and, for every \(x \in V(G)\), \(\deg (x) = d\).

Definition 14

We say \(G\) is locally bounded if it is locally finite and there exists a constant \(D\) such that, for all \(x \in V(G)\), \(\deg (x) \leq D\).

1.2 Adjacency operator

Let \(G\) be a graph. We will be interested in the Hilbert space \(\ell ^2(G) := \ell ^2(V(G))\), which is defined as the set of functions \(f : V(G) \rightarrow \mathbb {C}\) which are square-summable, equipped with the inner product

\[ \langle f, g \rangle = \sum _{x \in V(G)} f(x) \overline{g(x)}. \]

The space \(\mathcal{B}(\ell ^2(G))\) of bounded linear operators on \(\ell ^2(G)\) is a unital \(\mathbb {C}^*\)-algebra. Note that, in this context, \(0\) is the constant function equal to \(0\).

1.2.1 Constant fonctions

Definition 15

The constant function equal to \(1\) is defined by

\begin{equation} \mathbf{1}: \begin{cases} V(G) & \rightarrow \mathbb {C}\\ x & \mapsto 1. \end{cases} \end{equation}

Lemma 16

Assume \(G\) is not empty. Then the constant function \(\mathbf{1}\) is not equal to \(0\).

Proof ▶

If \(G\) is not empty, then by Definition 1, there exists \(x \in V(G)\). Then \(\mathbf{1}(x) = 1 \neq 0\), and hence \(\mathbf{1}\) is not equal to the constant function \(0\).

Lemma 17

The constant function \(\mathbf{1}\) belongs in \(\ell ^2(G)\) if and only if \(V(G)\) is finite.

1.2.2 Definition of the adjacency operator and elementary properties

Assume \(G\) is locally finite.

Definition 18

We define the adjacency operator \(a\) as the linear operator acting on the space of functions \(f : V(G) \rightarrow \mathbb {C}\) by

\[ a f (x) := \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} f(\mathrm{inc}\_ \mathrm{other}(e,x)). \]

Lemma 19

For any \(x \in V(G)\), \(a \mathbf{1}(x) = \deg (x)\).

Proof ▶

Let \(x \in V(G)\). We have

\begin{align*} a \mathbf{1}(x) & = \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)}\mathbf{1}(\mathrm{inc}\_ \mathrm{other}(e,x)) & \text{by Definition \ref{def:adjacency_operator}} \\ & = \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} & \text{by Definition \ref{def:constant_function}} \\ & = \deg (x) & \text{by Definition \ref{def:degree}}. \end{align*}

1.2.3 Norm of the adjacency operator

Let \(G\) be a locally finite graph. The aim of this subsection is to prove the following.

Proposition 20

Assume \(G\) is locally bounded. Then the adjacency operator is a bounded operator on \(\ell ^2(G)\) and its norm satisfies \(\| a\| \leq \sup _{x \in V(G)} \deg (x)\).

Here is a key lemma.

Lemma 21

For any function \(f : V(G) \rightarrow \mathbb {C}\), any vertex \(x \in V(G)\),

\begin{equation} |af(x)|^2 \leq \deg (x) \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} |f(\mathrm{inc}\_ \mathrm{other}(e,x))|^2. \end{equation}

Proof ▶

Let \(f : V(G) \rightarrow \mathbb {C}\) and \(x \in V(G)\). By Definition 18,

\begin{equation} |af(x)|^2 = \left| \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} f(\mathrm{inc}\_ \mathrm{other}(e, x))\right|^2. \end{equation}

By the Cauchy-Schwarz inequality,

\begin{equation*} |af(x)|^2 \leq \left(\sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} \right) \left( \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} |f(\mathrm{inc}\_ \mathrm{other}(e, x))|^2 \right). \end{equation*}

This leads to the claim by Definition 12.

Then Proposition 20 is a trivial consequence of the following lemma, together with the definition of bounded operator and operator norm.

Lemma 22

Assume \(G\) is locally bounded. Then, for any \(f \in \ell ^2(G)\), \(a f \in \ell ^2(G)\) and

\begin{equation} \| a f\| \leq \sup _{x \in V(G)} \deg (x) \times \| f\| . \end{equation}

Proof ▶

To write, basically we need to sum Lemma 21 for \(x \in V(G)\) (find the correct summation result), change the order of summation (same) and observe that

\begin{align*} \sum _{x \in V(G)} \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} |f(\mathrm{inc}\_ \mathrm{other}(e,x))|^2 & = \sum _{x \in V(G)} \deg (x) |f(x)|^2 \\ & \leq \sup _{x \in V(G)} \deg (x) \times \| f\| ^2. \end{align*}

1.2.4 Adjacency operator is self-adjoint

Let \(G\) be a locally bounded graph.

Proposition 23

The adjacency operator is selfadjoint.

The following lemma will be very handy.

Lemma 24

For any \(f\), \(g\) in \(\ell ^2(G)\),

\begin{equation} \langle af, g \rangle = \sum _{\substack {e \in E(G)\\ e \text{ links } x,y}} (f(x) \overline{g(y)} + f(y) \overline{g(x)}). \end{equation}

Proof ▶

Let \(f\), \(g\) be elements of \(\ell ^2(G)\). By Proposition 22, \(a f \in \ell ^2(G)\). By definition of the scalar product,

\begin{equation} \langle af, g \rangle = \sum _{x \in V(G)} af(x) \overline{g(x)}. \end{equation}

By Definition 18,

\begin{equation} \langle af, g \rangle = \sum _{x \in V(G)} \sum _{e \in \mathrm{incidenceSet}(x)} 2^{\mathrm{IsLoop}(e)} f(\mathrm{inc}\_ \mathrm{other}(e,x)) \overline{g(x)} \end{equation}

(todo: justify the change of order of summation, notably using Lemma 22 to have absolute convergence) which we can reorder to the result.

We are now ready to prove Proposition 23.

Proof ▶

Let \(f\), \(g\) be elements of \(\ell ^2(G)\). We have by Lemma 24

\begin{equation*} \langle af, g \rangle = \sum _{\substack {e \in E(G)\\ \begin{bgroup} e \text{ links } x,y \end{bgroup}}} (f(x) \overline{g(y)} + f(y) \overline{g(x)}) = \overline{\sum _{\substack {e \in E(G)\\ \begin{bgroup} e \text{ links } x,y \end{bgroup}}} (g(x) \overline{f(y)} + g(y) \overline{f(x)})} \end{equation*}

by complex conjugation, commutativity of addition and isLink_symm. Hence by Lemma 24

\begin{equation*} \langle af, g \rangle = \overline{\langle ag, f \rangle } = \langle f, ag \rangle \end{equation*}

by inner_conj_symm. This means that \(a^*=a\) by definition of the adjoint, which means \(a\) is self-adjoint by definition.

Corollary 25

The spectrum of the adjacency matrix is real.

Proof ▶

This follows from Proposition 23 with selfAdjoint.mem_spectrum_eq_re.

1.2.5 The case of regular graphs

Let \(d\) be a non-negative integer.

Lemma 26

Assume \(G\) is not empty and locally finite. Then \(G\) is regular of degree \(d\) iff \(a \mathbf{1}= d \mathbf{1}\).

Proof ▶

By Definition 13, \(G\) is regular of degree \(d\) if and only if for all \(x \in V(G)\), \(\deg (x)=d\). By Lemma 19, this is equivalent to having, for all \(x \in V(G)\), \(a \mathbf{1}(x) = d\), which is equivalent to \(a \mathbf{1}= d \mathbf{1}\) by Definition 15.

Lemma 27

If \(G\) is regular of degree \(d\), then \(\| a \| \leq d\).

Proof ▶

This is simply Proposition 20.

Lemma 28

If \(G\) is regular of degree \(d\), then the spectrum of \(a\) is included in the segment \([-d,d]\).

Proof ▶

By Corollary 25, the spectrum of \(a\) is real. By spectrum.subset_closedBall_norm, it is included in the closed ball of center \(0\) and radius \(\| a\| \). We have \(\| a\| \leq d\) by Lemma 27.

1.2.6 The case of finite graphs

Theorem 29

Assume \(G\) is finite and let \(n\) denote the cardinal of \(V(G)\). Then the spectrum of the adjacency operator is a family of \(n\) real eigenvalues

\[ \lambda _1 \geq \lambda _2 \geq \ldots \geq \lambda _n. \]

Proof ▶

This is the spectral theorem in finite dimension.

1.2.7 The case of finite regular graphs

Let \(d\) be a non-negative integer.

Lemma 30

Assume \(G\) is regular of degree \(d\) and finite. Then \(d\) is an eigenvalue of the adjacency operator with associated eigenfunction the constant function \(\mathbf{1}\).

Proof ▶

Since \(G\) is finite, \(\mathbf{1}\in \ell ^2(G)\) by Lemma 17. Furthermore, \(\mathbf{1}\neq 0\) by Lemma 16 and since \(G\) is not empty by Definition 13. By Lemma 26, if \(G\) is regular of degree \(d\), then \(a \mathbf{1}= d \mathbf{1}\). We conclude by the definition of eigenvalue and eigenvector.

Proposition 31

If \(G\) is finite and regular of degree \(d\), then \(\| a\| =d\).

Proof ▶

Since \(G\) is regular of degree \(d\), by Lemma 27, \(\| a \| \leq d\). By Lemma 30, \(d\) is an eigenvalue of \(a\) and hence \(\| a\| \geq d\), which is enough to conclude.

Proposition 32

Let \(G\) be a regular graph of degree \(d\). Assume \(G\) is finite with \(n\) vertices. Let \(m\) be the number of connected components of \(G\). Then \(\lambda _i = d\) for all \(i \in \{ 1, \ldots , m\} \).

Proof ▶

todo

Proposition 33

Let \(G\) be a regular graph of degree \(d\). Assume \(G\) is finite with \(n\) vertices. Then \(\lambda _n = -d\) iff the graph is bipartite.

Proof ▶

todo