We have \(\mathrm{edge}(\mathrm{symm}(\mathrm{symm}(d))) = \mathrm{edge}(\mathrm{symm}(d)) = \mathrm{edge}(d)\) so have \(\mathrm{symm}(\mathrm{symm}(d))=d\) or \(\mathrm{symm}(\mathrm{symm}(d))=\mathrm{symm}(d)\). The latter is impossible due to \(\mathrm{symm}\) having no fixed point.

We start by proving (1) \(\Rightarrow \) (2). Assume \(x\) and \(y\) are adjacent. Then there exists an edge \(e\) linking \(x\) and \(y\). The function \(\mathrm{edge}\) is surjective so there exists \(d \in D(G)\) such that \(\mathrm{edge}(d)=e\). \(e\) links \(x\) and \(y\) but also \(\mathrm{start}(d)\) and \(\mathrm{end}(d)\) so:

• either \(x=\mathrm{start}(d)\) and \(y=\mathrm{end}(d)\), in which case \(d \in \mathrm{dartSet}(x)\) satisfies the claim;

• otherwise \(x = \mathrm{end}(d) = \mathrm{start}(\mathrm{symm}(d))\) and \(y = \mathrm{start}(d) = \mathrm{end}(\mathrm{symm}(d))\) and hence \(\mathrm{symm}(d) \in \mathrm{dartSet}(x)\) satisfies the claim.

The implication (2) \(\Rightarrow \) (3) is immediate by definition of \(\mathrm{dartSet}(x,y)\).

To conclude, (3) \(\Rightarrow \) (1) because, if \(d \in \mathrm{dartSet}(x,y)\), then \(\mathrm{edge}(d)\) links \(x\) and \(y\) and hence they are adjacent.

Let \(e \in E(G)\). The map \(\mathrm{edge}\) is surjective so there exists \(d \in D(G)\) such that \(\mathrm{edge}(d)=e\). We have \(\mathrm{edge}(\mathrm{symm}(d))=\mathrm{edge}(d)=e\). This proves \(\{ d, \mathrm{symm}(d)\} \subseteq \mathrm{edge}^{-1}(\{ e\} )\). For the other direction, if \(d' \in D(G)\) satisfies \(\mathrm{edge}(d')=e\), then \(\mathrm{edge}(d)=\mathrm{edge}(d')\) which implies by definition that \(d'=d\) or \(d'=\mathrm{symm}(d)\), which is the claim.

Let \(d \in \mathrm{dartSet}(x,y)\). Then, \(\mathrm{edge}(d) \in E(G)\) links \(\mathrm{start}(d)=x\) and \(\mathrm{end}(d)=y\). So \(\mathrm{edge}(d)\) belongs in the claimed set.

Now take \(e \in E(G)\) linking \(x\) and \(y\). By Lemma 6, there exists \(d \in D(G)\) such that \(\mathrm{edge}^{-1}(\{ e\} ) = \{ d, \mathrm{symm}(d)\} \). We check that \(d\) or \(\mathrm{symm}(d)\) belongs in \(\mathrm{dartSet}(x,y)\), and that both of them do iff \(x=y\), which leads to the claim.

This is a classic fact for involutions with no fixed points.

The only thing to check is that the definition of the links does not depend on the choice of a representative, which is true since \(\mathrm{start}\circ \mathrm{symm}= \mathrm{end}\) and \(\mathrm{end}\circ \mathrm{symm}= \mathrm{start}\).

The reachability relation is reflexive: \(x \sim x\) for any \(x \in V(G)\). Indeed, let \(x \in V(G)\). We take \(m=0\) and set \(v_0=x\). Then this is a walk from \(x\) to \(x\) on \(G\).

The reachability relation is symmetric: if \(x \sim y\) then \(y \sim x\). Let \(x\), \(y\) be two vertices. We assume \(x \sim y\). Let \((v_i)_{0 \leq i \leq m}\) and \((e_i)_{1 \leq i \leq m}\) be a walk from \(x\) to \(y\). Then \((v_{m-i})_{0 \leq i \leq m}\) and \((e_{m+1-i})_{1 \leq i \leq m}\) is a walk from \(y\) to \(x\). So \(y \sim x\).

The reachability relation is transitive: if \(x \sim y\) and \(y \sim z\) then \(x \sim z\). Assume \(x \sim y\) and \(y \sim z\). Let \((v_i)_{0 \leq i \leq m}\) and \((e_i)_{1 \leq i \leq m}\) be a walk from \(x\) to \(y\) and \((v_i')_{0 \leq i \leq m'}\), \((e_i')_{1 \leq i \leq m'}\) be a walk from \(y\) to \(z\). We let \(m''=m+m'\) and define for \(i \in \{ 0, \ldots , m'\} \)

and for \(i \in \{ 1, \ldots , m'\} \)

Then this is a walk from \(x\) to \(z\), hence \(x \sim z\).

By definition of adjacency, there exists an edge \(e \in E(G)\) linking \(x\) and \(y\). Then the walk \((x, y)\) and \((e)\) is a walk from \(x\) to \(y\).

Using Lemma 7,

which leads to the desired equality. Hence \(G\) is locally finite at \(x\) iff \(\mathrm{incidenceSet}(x)\) and \(\mathrm{loopSet}(x)\) are both finite, which is equivalent to \(\mathrm{incidenceSet}(x)\) being finite as \(\mathrm{loopSet}(x) \subseteq \mathrm{incidenceSet}(x)\).

Take \(y \in C_{r+1}(x)\). Then there exists a walk \((v_i)_{0 \leq i \leq r+1}\), \((e_i)_{1 \leq i \leq r+1}\) from \(x\) to \(y\). We take \(z=v_{r}\) and check it is adjacent to \(y\) and lies in \(C_r(x)\).

todo

To be adapted from SimpleGraph.

Let \(x, y \in V(G)\). By definition of the diameter, \(\mathrm{dist}(x,y) \leq \mathrm{diam}(G)\) and hence \(y\) lies in the ball of radius \(\mathrm{diam}(G)\) centered at \(x\).

Let \(x \in V(G)\). By Lemma 62, if \(r := \mathrm{diam}(G)\), then \(V(G) \subseteq B_r(x)\). In particular \(\# V(G) \leq \# B_r(X) \leq \delta ^r\) by Proposition 58.

If \(V(G)\) is not empty, then there exists \(x \in V(G)\). Then \(\mathbf{1}(x) = 1 \neq 0\), and hence \(\mathbf{1}\neq 0\).

We directly check that:

• the constant function equal to \(0\) is constant;

• for any constant functions \(f_1\), \(f_2\) and any \(c \in \mathbb {C}\), the function \(f_1+cf_2\) is also constant;

both by direct application of the definition. We also check that the function \(\mathbf{1}\) is constant.

Let \(f : V(G) \rightarrow \mathbb {C}\) be a constant function. Since \(V(G)\) is not empty there exists \(x \in V(G)\). Then for all \(y \in V(G), f(y) = f(x) \mathbf{1}(y)\), so \(f = f(x) \mathbf{1}\), which allows to conclude.

By definition of the orthogonal, \(\mathbf{1}^\perp \) is the space of functions \(f \in \ell ^2(G)\) such that \(\langle f, \mathbf{1}\rangle = 0\). Since \(V(G)\) is finite all functions \(V(G) \rightarrow \mathbb {C}\) are in \(\ell ^(G)\). By definition of the scalar product and the constant function, \(\langle f, \mathbf{1}\rangle = \sum _{x \in V(G)}f(x)\).

By induction.

Let \(G\) be a preconnected graph and \(f : V(G) \rightarrow \mathbb {C}\) be a locally constant function. For any \(x\), \(y\) in \(V(G)\), by Definition 29, there exists a walk from \(x\) to \(y\). Lemma 75 this implies \(f(x)=f(y)\). Hence by Definition 64, \(f\) is constant.

Let \(f\) be a locally constant function on \(G\), and \(H\) be a subgraph of \(G\). Let \(x, y\) be adjacent vertices in \(H\). By Lemma 14, \(x\) and \(y\) are also adjacent in \(G\). Then \(f(x)=f(y)\).

Assume \(f\) is locally constant. Let \(C\) be a connected component of \(G\). By Lemma 77, the restriction of \(f\) to \(C\) is locally constant. By Theorem 35, \(C\) is preconnected. So by Lemma 76, the restriction of \(f\) to \(C\) is constant.

Assume the restriction of \(f\) to each connected component is constant. Let \(x\), \(y\) be adjacent vertices. Then by Lemma 34, \(\mathrm{cc}(x) = \mathrm{cc}(y)\) which implies that \(y \in \mathrm{cc}(x)\). This allows to conclude since \(f\) is constant on \(\mathrm{cc}(x)\) by hypothesis and Theorem 35.

We directly check that:

• the constant function equal to \(0\) is locally constant;

• for any locally constant functions \(f_1\), \(f_2\) and any \(c \in \mathbb {C}\), the function \(f_1+cf_2\) is also locally constant;

both by direct application of the definition.

Now, for any connected component \(C\), \(\mathbf{1}_C\) is locally constant by Lemma 79.

We prove these functions form a basis using the fact that, by Proposition 37 and Lemma 72,

and hence if \(f\) is locally constant,

The function \(f\) is constant on each connected component so this is a decomposition in the desired basis. The decomposition is unique as for all \(x \in V(G)\), the coefficient associated to \(\mathrm{cc}(x)\) must be \(f(x)\) since \(\mathbf{1}_C(x)=0\) for all other connected component.

Let \(x \in V(G)\). By definition,

By Lemma 5, for all \(d \in \mathrm{dartSet}(x)\), \(\mathrm{end}(d)\) is adjacent to \(x\) and in particular \(f(\mathrm{end}(d))=f(x)\). This leads to the conclusion by Definition 41.

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

By the Cauchy-Schwarz inequality applied to the complex vectors \(v_1 := (1)_{d \in \mathrm{dartSet}(x)}\) and \(v_2 := (f(\mathrm{end}(d)))_{d \in \mathrm{dartSet}(x)}\) we have

This leads to the inequality by Definition 41. The equality case comes from the equality case in Cauchy-Schwarz, which occurs if and only if the vectors \(v_1\) and \(v_2\) are colinear, which is equivalent to the announced condition as \(v_1\) is a non-zero constant vector, using Lemma 5.

Let us write \(D := \sup _{x \in V(G)} \deg (x)\). By definition,

and \(af \in \ell ^2(G)\) iff this sum is finite. We sum Lemma 86 for all vertices of \(G\) and obtain that

We apply the involution \(\mathrm{symm}\) to the sum, changing indices, to obtain

Now by Definitions 3 and 41

This means that \(af \in \ell ^2(G)\) and \(\| af\| \leq D \| f\| \), which was our claim. If the equality occurs, since all terms are non-negative, it means that \(\deg (x)\) is constant (i.e. the graph is regular), and that there is equality in each term of Lemma 86, which is the conclusion.

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

By Definition 82,

which we can rewrite as the claim.

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

by complex conjugation and applying the involution \(\mathrm{symm}\) to exchange the start and end of each dart. Hence by Lemma 89

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

This follows from Proposition 88 with selfAdjoint.mem_spectrum_eq_re.

By Corollary 90, 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 Theorem 85.

If \(V(G)\) is finite, then \(\ell ^2(G)\) has finite dimension. So this is just the spectral theorem for self-adjoint operators in finite dimension.

The functions \(\mathbf{1}_{\{ x\} }\) and \(\mathbf{1}_{\{ y\} }\) are trivially in \(\ell ^2(G)\). By Lemma 89,

which is exactly the claim by Definition 4 and Definition 70.

By Lemma 93, this quantity is a cardinal of a set, and hence a non-negative integer. The parity when \(x=y\) comes from Lemma 42.

We check that

and

and

We have by definition of the adjacency operator for a function \(f : V \rightarrow \mathbb {C}\) and \(x \in V\),

which leads to the conclusion as we recognise \(u_{\pi _i}\) and \(u_{\pi _i^{-1}} = u_{\pi _i}^*\).