Relabelling darts and padding with loops #

Two bookkeeping operations on regular graphs, both preserving the spectral bound in an explicit way.

Relabelling the dart type along an equivalence. Constructions produce structured dart types — pairs, functions, sums — while ExpanderFamily wants Fin degree. The step operator is unchanged, so the bound is.
Padding with self-loops, to raise the degree of a graph to a prescribed value. The new step is a convex combination of the old step and the identity, so by Jensen the bound becomes μ² = α λ² + (1 - α) with α the fraction of real darts.

Main definitions #

Complexity.RegGraph.relabel — the same graph with darts renamed
Complexity.RegGraph.padLoops — the graph with k self-loops added at every vertex

Main results #

Complexity.RegGraph.spectralBound_relabel
Complexity.RegGraph.spectralBound_padLoops
Complexity.RegGraph.relabelV, Complexity.RegGraph.spectralBound_relabelV — renaming vertices
Complexity.RegGraph.toFinForm — the same graph with both types numbered

Relabelling #

source

def Complexity.RegGraph.relabel (G : RegGraph) {D' : Type} [DecidableEq D'] [Fintype D'] (e : G.D ≃ D') :

RegGraph

The same graph with its darts renamed along e.

Equations

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

Instances For

source

@[simp]

theorem Complexity.RegGraph.order_relabel (G : RegGraph) {D' : Type} [DecidableEq D'] [Fintype D'] (e : G.D ≃ D') :

(G.relabel e).order = G.order

source

theorem Complexity.RegGraph.deg_relabel (G : RegGraph) {D' : Type} [DecidableEq D'] [Fintype D'] (e : G.D ≃ D') :

(G.relabel e).deg = G.deg

source

theorem Complexity.RegGraph.step_relabel (G : RegGraph) {D' : Type} [DecidableEq D'] [Fintype D'] (e : G.D ≃ D') (f : G.V → ℝ) (v : G.V) :

(G.relabel e).step f v = G.step f v

source

theorem Complexity.RegGraph.spectralBound_relabel (G : RegGraph) {D' : Type} [DecidableEq D'] [Fintype D'] (e : G.D ≃ D') {lam : ℝ} (h : G.SpectralBound lam) :

(G.relabel e).SpectralBound lam

Padding with loops #

source

def Complexity.RegGraph.padLoops (G : RegGraph) (k : ℕ) :

RegGraph

The graph with k self-loops added at every vertex.

Equations

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

Instances For

source

@[simp]

theorem Complexity.RegGraph.order_padLoops (G : RegGraph) (k : ℕ) :

(G.padLoops k).order = G.order

source

theorem Complexity.RegGraph.deg_padLoops (G : RegGraph) (k : ℕ) :

(G.padLoops k).deg = G.deg + k

source

theorem Complexity.RegGraph.step_padLoops (G : RegGraph) (k : ℕ) (f : G.V → ℝ) (v : G.V) :

(G.padLoops k).step f v = (↑G.deg * G.step f v + ↑k * f v) / (↑G.deg + ↑k)

source

theorem Complexity.RegGraph.spectralBound_padLoops (G : RegGraph) (k : ℕ) {lam : ℝ} (h : G.SpectralBound lam) :

(G.padLoops k).SpectralBound √((↑G.deg * lam ^ 2 + ↑k) / (↑G.deg + ↑k))

Padding keeps the bound, with μ² = α λ² + (1 - α) for α the fraction of real darts.

Renaming vertices #

source

def Complexity.RegGraph.relabelV (G : RegGraph) {V' : Type} [DecidableEq V'] [Fintype V'] (e : G.V ≃ V') :

RegGraph

The same graph with its vertices renamed along e. Constructions produce structured vertex types — products, sums — while a family wants Fin n.

Equations

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

Instances For

source

@[simp]

theorem Complexity.RegGraph.deg_relabelV (G : RegGraph) {V' : Type} [DecidableEq V'] [Fintype V'] (e : G.V ≃ V') :

(G.relabelV e).deg = G.deg

source

theorem Complexity.RegGraph.order_relabelV (G : RegGraph) {V' : Type} [DecidableEq V'] [Fintype V'] (e : G.V ≃ V') :

(G.relabelV e).order = G.order

source

theorem Complexity.RegGraph.step_relabelV (G : RegGraph) {V' : Type} [DecidableEq V'] [Fintype V'] (e : G.V ≃ V') (f : V' → ℝ) (v : V') :

(G.relabelV e).step f v = G.step (fun (w : G.V) => f (e w)) (e.symm v)

source

theorem Complexity.RegGraph.spectralBound_relabelV (G : RegGraph) {V' : Type} [DecidableEq V'] [Fintype V'] (e : G.V ≃ V') {lam : ℝ} (h : G.SpectralBound lam) :

(G.relabelV e).SpectralBound lam

Numbering both types #

source

noncomputable def Complexity.RegGraph.toFinForm (G : RegGraph) :

RegGraph

The same graph with its vertices numbered Fin order and its darts Fin deg. Constructions build structured types; the merge and the expander families want numbered ones.

Equations

G.toFinForm = (G.relabelV (Fintype.equivFin G.V)).relabel (Fintype.equivFin G.D)

Instances For

source

@[simp]

theorem Complexity.RegGraph.order_toFinForm (G : RegGraph) :

G.toFinForm.order = G.order

source

@[simp]

theorem Complexity.RegGraph.deg_toFinForm (G : RegGraph) :

G.toFinForm.deg = G.deg

source

theorem Complexity.RegGraph.spectralBound_toFinForm (G : RegGraph) {lam : ℝ} (h : G.SpectralBound lam) :

G.toFinForm.SpectralBound lam

source

noncomputable def Complexity.RegGraph.toFinFormOf (G : RegGraph) (N d : ℕ) (hN : Fintype.card G.V = N) (hd : Fintype.card G.D = d) :

RegGraph

The same graph numbered at sizes supplied by the caller, so that the rotation map has the literal type Fin N × Fin d → Fin N × Fin d a numeric construction expects, with no transport at the use site.

Equations