The complete graph with self-loops

The simplest nontrivial RegGraph: n vertices, degree n, with the i-th neighbour of every vertex being i. Its rotation map is the swap, so every vertex is joined to every vertex including itself.

It is a perfect expander: one step of its walk lands on the uniform distribution, so the walk operator annihilates mean-zero functions and SpectralBound 0 holds. This validates the definitions in RegularGraph on a case where the answer is known, and supplies the loops that WalkPath needs.

Main definitions

• RegGraph.cliqueLoops — the complete graph with all self-loops
• RegGraph.cliqueLoopsLoops — its canonical self-loop at each vertex

Main results

• RegGraph.nbr_cliqueLoops, RegGraph.step_cliqueLoops
• RegGraph.spectralBound_cliqueLoops — a spectral bound of 0

def Complexity.RegGraph.cliqueLoops (n : ℕ) (hn : 0 < n) : RegGraph

The complete graph on n vertices with a self-loop at every vertex, presented by the swap rotation map: the i-th neighbour of v is i.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.RegGraph.V_cliqueLoops (n : ℕ) (hn : 0 < n) : (cliqueLoops n hn).V = Fin n

@[simp]

theorem Complexity.RegGraph.D_cliqueLoops (n : ℕ) (hn : 0 < n) : (cliqueLoops n hn).D = Fin n

@[simp]

theorem Complexity.RegGraph.deg_cliqueLoops (n : ℕ) (hn : 0 < n) : (cliqueLoops n hn).deg = n

@[simp]

theorem Complexity.RegGraph.order_cliqueLoops (n : ℕ) (hn : 0 < n) : (cliqueLoops n hn).order = n

@[simp]

theorem Complexity.RegGraph.nbr_cliqueLoops {n : ℕ} (hn : 0 < n) (v : (cliqueLoops n hn).V) (i : (cliqueLoops n hn).D) : (cliqueLoops n hn).nbr v i = i

def Complexity.RegGraph.cliqueLoopsLoops (n : ℕ) (hn : 0 < n) : (cliqueLoops n hn).Loops

Every vertex of the complete graph with loops has a self-loop, namely its own index.

Equations

• Complexity.RegGraph.cliqueLoopsLoops n hn = { loop := fun (v : (Complexity.RegGraph.cliqueLoops n hn).V) => v, rot_loop := ⋯ }

theorem Complexity.RegGraph.step_cliqueLoops {n : ℕ} (hn : 0 < n) (f : (cliqueLoops n hn).V → ℝ) (v : (cliqueLoops n hn).V) : (cliqueLoops n hn).step f v = (∑ w : (cliqueLoops n hn).V, f w) / ↑(cliqueLoops n hn).deg

One step of the walk lands on the uniform distribution: the average of f over all vertices, whatever the current vertex.

theorem Complexity.RegGraph.spectralBound_cliqueLoops {n : ℕ} (hn : 0 < n) : (cliqueLoops n hn).SpectralBound 0

The complete graph with loops is a perfect expander.