Formalization of the book's content

References

• [Spectral Graph Theory, Fan Chung][Chung]

structure WeightedGraph (α : Type u_1) (β : Type u_2) extends Graph α β : Type (max u_1 u_2)

• vertexSet : Set α
• IsLink : β → α → α → Prop
• edgeSet : Set β
• isLink_symm ⦃e : β⦄ : e ∈ self.edgeSet → Symmetric (self.IsLink e)
• eq_or_eq_of_isLink_of_isLink ⦃e : β⦄ ⦃x y v w : α⦄ : self.IsLink e x y → self.IsLink e v w → x = v ∨ x = w
• edge_mem_iff_exists_isLink (e : β) : e ∈ self.edgeSet ↔ ∃ (x : α) (y : α), self.IsLink e x y
• left_mem_of_isLink ⦃e : β⦄ ⦃x y : α⦄ : self.IsLink e x y → x ∈ self.vertexSet
• edgeWeight : β → NNReal
• edgeDef (e : β) : e ∈ self.edgeSet ↔ 0 < self.edgeWeight e
• orientation : β → α

noncomputable def WeightedGraph.degree {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (v : α) : NNReal

G.degree v is the number of edges incident to v.

Equations

• WeightedGraph.degree v = ↑(Graph.incidenceSet v).ncard

def WeightedGraph.IsRegularOfDegree {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (k : ℕ) : Prop

A graph is regular of degree d if every vertex has degree d.

Equations

• WeightedGraph.IsRegularOfDegree k = ∀ (v : α), WeightedGraph.degree v = ↑k

noncomputable def WeightedGraph.graphVolume {α : Type u_1} {β : Type u_2} [Fintype α] {G : WeightedGraph α β} : NNReal

The volume of a graph is defined as the sum of the degrees of its vertices

Equations

• WeightedGraph.graphVolume = ∑ v : α, WeightedGraph.degree v

noncomputable def WeightedGraph.vol {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (S : Set α) [Fintype ↑S] : NNReal

We define vol S, the volume of S, to be the sum of the degrees of the vertices in S.

Equations

• WeightedGraph.vol S = ∑ v : ↑S, WeightedGraph.degree ↑v

def WeightedGraph.IsIsolated {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} (v : ↑G.vertexSet) : Prop

We say v is an isolated vertex if dᵥ = 0.

Equations

• WeightedGraph.IsIsolated v = (WeightedGraph.degree ↑v = 0)

theorem WeightedGraph.no_adj_iff_zero_degree {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (v : α) : degree v = 0 ↔ ∀ (u : α), ¬G.Adj u v

A vertex has degree 0 iff it has no adjacent vertex.

def WeightedGraph.NonTrivial {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

A graph is said to be nontrivial if it contains at least one edge.

Equations

• WeightedGraph.NonTrivial G = (G.edgeSet ≠ ∅)

noncomputable def WeightedGraph.L {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : WeightedGraph α β} [DecidableRel G.Adj] : Matrix α α ℝ

Equations

• WeightedGraph.L u v = if u = v then ↑(WeightedGraph.degree v) else if G.Adj u v then -1 else 0

noncomputable def WeightedGraph.Laplacian {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : WeightedGraph α β} [DecidableRel G.Adj] : Matrix α α ℝ

Equations

• WeightedGraph.Laplacian u v = if u = v then if WeightedGraph.degree v = 0 then 0 else 1 else if G.Adj u v then -1 / √(↑(WeightedGraph.degree v) * ↑(WeightedGraph.degree u)) else 0

noncomputable def WeightedGraph.T_sqrt {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : WeightedGraph α β} : Matrix α α ℝ

Equations

• WeightedGraph.T_sqrt = Matrix.diagonal fun (v : α) => √↑(WeightedGraph.degree v)

noncomputable def WeightedGraph.T_inv_sqrt {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : WeightedGraph α β} : Matrix α α ℝ

Equations

• WeightedGraph.T_inv_sqrt = Matrix.diagonal fun (v : α) => if WeightedGraph.degree v = 0 then 0 else 1 / √↑(WeightedGraph.degree v)

theorem WeightedGraph.Lap_symmetric_normalization {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] : Laplacian = T_inv_sqrt * L * T_inv_sqrt

Laplacian = T_inv_sqrt * L * T_inv_sqrt

noncomputable def WeightedGraph.LapOperator {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] {G : WeightedGraph α β} [DecidableRel G.Adj] : (α → ℝ) →L[ℝ] α → ℝ

The Laplacian can be viewed as an operator on the space of functions g : V(G) → R.

Equations

• WeightedGraph.LapOperator = LinearMap.toContinuousLinearMap (Matrix.toLin' WeightedGraph.Laplacian)

def WeightedGraph.IsSimple {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} : Prop

No multiple loops

Equations

• WeightedGraph.IsSimple = ∀ (u : α), ↑(WeightedGraph.degree u) = ↑{v : α | G.Adj u v}.ncard

theorem WeightedGraph.LapOperatorFormula {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hS : IsSimple) : ⇑LapOperator = fun (g : α → ℝ) (u : α) => 1 / √↑(degree u) * ∑ v : α, if G.Adj u v then g u / √↑(degree u) - g v / √↑(degree v) else 0

The Laplacian Operator satisfies big equation page 3.

def WeightedGraph.Adjacency {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} [DecidableRel G.Adj] : Matrix α α ℝ

Adjacency Matrix: A(u, v) = 1 if u is adjacent to v, and 0 otherwise.

Equations

• WeightedGraph.Adjacency u v = if G.Adj u v then 1 else 0

@[reducible, inline]

abbrev WeightedGraph.Identity {α : Type u_1} [DecidableEq α] : Matrix α α ℝ

Equations

• WeightedGraph.Identity = 1

theorem WeightedGraph.LapOfRegGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] {k : ℕ+} (hLoopless : ∀ (v : α), ¬G.Adj v v) : IsRegularOfDegree ↑k → Laplacian = Identity - (1 / ↑↑k) • Adjacency

For a loopless, k-regular graph, Laplacian = Identity − 1/k * Adjacency

def WeightedGraph.NoIsolation {α : Type u_1} {β : Type u_2} {G : WeightedGraph α β} : Prop

We say that a graph has no isolation when none of its vertices is isolated.

Equations

• WeightedGraph.NoIsolation = ∀ (v : ↑G.vertexSet), ¬WeightedGraph.IsIsolated v

theorem WeightedGraph.LapOfNotIsolatedGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hα : G.vertexSet = Set.univ) (hLoopless : ∀ (v : α), ¬G.Adj v v) : NoIsolation → Laplacian = Identity - T_inv_sqrt * Adjacency * T_inv_sqrt

For a graph without isolated vertices, we have Laplacian = Identity - T_inv_sqrt * Adjacency * T_inv_sqrt.

noncomputable def WeightedGraph.S {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : WeightedGraph α β} [DecidableRel G.Inc] : Matrix α β ℝ

S is the matrix whose rows are indexed by the vertices and whose columns are indexed by the edges of G. Each column corresponding to an edgece = {u, v} has an entry 1/√dᵤ in the row corresponding to u, an entry −1/√dᵥ in the row corresponding to v, and has zero entries elsewhere.

Equations

• WeightedGraph.S u e = if G.Inc e u then if G.orientation e = u then 1 / √↑(WeightedGraph.degree u) else -1 / √↑(WeightedGraph.degree u) else 0

theorem WeightedGraph.LSS {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] [DecidableRel G.Inc] : Laplacian = S * S.transpose

Laplacian = S * Sᵀ

theorem WeightedGraph.LapHermitian {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] : Laplacian.IsHermitian

Proof that the Laplacian as defined above, is Hermitian.

noncomputable def WeightedGraph.lapEigvals {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] : Fin (Fintype.card α) → ℝ

Eigenvalues of the Laplacian Matrix in non-increasing order.

Equations

• WeightedGraph.lapEigvals i = ⋯.eigenvalues₀ i.rev

def WeightedGraph.DirichletSum {α : Type u_1} {β : Type u_2} [Fintype α] {G : WeightedGraph α β} [DecidableRel G.Adj] (f : α → ℝ) : ℝ

The Dirichlet sum of a graph G is the sum of (f(u) - f(v))² over all unordered pairs {u, v} for which u and v are adjacent.

Equations

• WeightedGraph.DirichletSum f = ∑ u : α, ∑ v : α, if G.Adj u v then (f u - f v) ^ 2 else 0

def WeightedGraph.lapSpectrum {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] (G : WeightedGraph α β) [DecidableRel G.Adj] : Set ℝ

The spectrum of a graph

Equations

• G.lapSpectrum = spectrum ℝ WeightedGraph.Laplacian

@[reducible, inline]

abbrev WeightedGraph.τ {α : Type u_1} : α → ℝ

τ denote the constant function which assigns the value 1 on each vertex

Equations

• WeightedGraph.τ x✝ = 1

theorem WeightedGraph.card_of_adj_loopless {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (v : α) (hS : IsSimple) : ↑{x : α | G.Adj v x}.ncard = degree v

theorem WeightedGraph.adj_degree_neq_zero {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (u v : α) (hAdj : G.Adj u v) : degree u ≠ 0 ∧ degree v ≠ 0

theorem WeightedGraph.zero_eigenvalue_normalized {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hS : IsSimple) (hLoopless : ∀ (v : α), ¬G.Adj v v) : Laplacian.mulVec (T_sqrt.mulVec τ) = 0

T_sqrt * τ is an eigenfunction of Laplacian with eigenvalue 0.

@[reducible, inline]

abbrev WeightedGraph.hGH {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] : Laplacian.IsHermitian

Equations

• ⋯ = ⋯

theorem WeightedGraph.eigval_order {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] [OfNat (Fin (Fintype.card α)) 1] {i j : Fin (Fintype.card α)} : i ≤ j → lapEigvals i ≤ lapEigvals j

Helper to access the eigenvalues by non-decreasing order.

structure WeightedGraph.CompleteGraph (α : Type u_3) (β : Type u_4) extends WeightedGraph α β : Type (max u_3 u_4)

Complete Graph Kₙ on n vertices.

• vertexSet : Set α
• IsLink : β → α → α → Prop
• edgeSet : Set β
• isLink_symm ⦃e : β⦄ : e ∈ self.edgeSet → Symmetric (self.IsLink e)
• eq_or_eq_of_isLink_of_isLink ⦃e : β⦄ ⦃x y v w : α⦄ : self.IsLink e x y → self.IsLink e v w → x = v ∨ x = w
• edge_mem_iff_exists_isLink (e : β) : e ∈ self.edgeSet ↔ ∃ (x : α) (y : α), self.IsLink e x y
• left_mem_of_isLink ⦃e : β⦄ ⦃x y : α⦄ : self.IsLink e x y → x ∈ self.vertexSet
• edgeWeight : β → NNReal
• edgeDef (e : β) : e ∈ self.edgeSet ↔ 0 < self.edgeWeight e
• orientation : β → α
• completeness (x y : α) : x ≠ y ↔ ∃ (e : ↑self.edgeSet), self.IsLink (↑e) x y

theorem WeightedGraph.complete_graph_loopless {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] [OfNat (Fin (Fintype.card α)) 1] {K : CompleteGraph α β} (v : α) : ¬K.Adj v v

theorem WeightedGraph.zero_mem_spectrum_lapMatrix {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] [OfNat (Fin (Fintype.card α)) 1] (K : CompleteGraph α β) [DecidableRel K.Adj] : 0 ∈ K.lapSpectrum

0 is an eigenvalue of the Laplacian of a graph.

theorem WeightedGraph.zero_mem_complete_graph_spectrum {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] [OfNat (Fin (Fintype.card α)) 1] (K : CompleteGraph α β) [DecidableRel K.Adj] : 0 ∈ K.lapSpectrum

For the complete graph Kₙ on n vertices, the eigenvalues are 0 and n/(n − 1) (with multiplicity n − 1).

theorem WeightedGraph.lapEigvals_sum_eq_trace {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hα : G.vertexSet = Set.univ) {n : ℕ} (hn : n = Nat.card ↑G.vertexSet) [Fact (1 < n)] [OfNat (Fin (Fintype.card α)) 1] : ∑ i : Fin (Fintype.card α), lapEigvals i = Laplacian.trace

theorem WeightedGraph.eigval_sum_le_n {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hα : G.vertexSet = Set.univ) {n : ℕ} (hn : n = Nat.card ↑G.vertexSet) [Fact (1 < n)] [OfNat (Fin (Fintype.card α)) 1] : ∑ i : Fin (Fintype.card α), lapEigvals i ≤ ↑n

For graph G on n vertices, the sum of its eigenvalues it at most n.

theorem WeightedGraph.eigval_sum_eq_n_iff_no_isolation {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hα : G.vertexSet = Set.univ) {n : ℕ} (hn : n = Nat.card ↑G.vertexSet) [Fact (1 < n)] [OfNat (Fin (Fintype.card α)) 1] (h : NoIsolation) : ∑ i : Fin (Fintype.card α), lapEigvals i = ↑n

The equality in eigval_sum_le_n holds iff G has NoIsolation.

theorem WeightedGraph.second_eigval_le_div {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : WeightedGraph α β} [DecidableRel G.Adj] (hα : G.vertexSet = Set.univ) {n : ℕ} (hn : n = Nat.card ↑G.vertexSet) [Fact (1 < n)] [OfNat (Fin (Fintype.card α)) 1] : lapEigvals 1 ≤ ↑n / (↑n - 1)

Second eigenvalue is at most n / n-1.