Formalization of the book's content

References

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

structure UnweightedGraph (α : 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
• orientation : β → α

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

noncomputable def UnweightedGraph.vol {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} (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

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

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

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

Equations

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

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

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

def UnweightedGraph.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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Laplacian = T_inv_sqrt * L * T_inv_sqrt

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

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

Equations

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

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

No multiple loops

Equations

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

theorem UnweightedGraph.LapOperatorFormula {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] (hS : IsSimple) (hLoopless : ∀ (v : α), ¬G.Adj v v) : ⇑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 UnweightedGraph.Adjacency {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} [DecidableRel G.Adj] : Matrix α α ℝ

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

Equations

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

@[reducible, inline]

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

Equations

• UnweightedGraph.Identity = 1

theorem UnweightedGraph.LapOfRegGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] {G : UnweightedGraph α β} [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 UnweightedGraph.NoIsolation {α : Type u_1} {β : Type u_2} {G : UnweightedGraph α β} : Prop

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

Equations

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

theorem UnweightedGraph.LapOfNotIsolatedGraph {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [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 UnweightedGraph.S {α : Type u_1} {β : Type u_2} [DecidableEq α] {G : UnweightedGraph α β} [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

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

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

Laplacian = S * Sᵀ

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

Proof that the Laplacian as defined above, is Hermitian.

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

Eigenvalues of the Laplacian Matrix in non-increasing order.

Equations

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

def UnweightedGraph.DirichletSum {α : Type u_1} {β : Type u_2} [Fintype α] {G : UnweightedGraph α β} [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

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

theorem UnweightedGraph.lapEigvals_one_eq_inf_rayleigh {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] [Nonempty α] (hS : IsSimple) (hLoopless : ∀ (v : α), ¬G.Adj v v) : lapEigvals 1 = ⨅ (f : α → ℝ), ⨅ (_ : ∑ v : α, f v * ↑(degree v) = 0), ⨅ (_ : f ≠ 0), 1 / 2 * DirichletSum f / ∑ v : α, f v ^ 2 * ↑(degree v)

Quotient de Rayleigh pour la première valeur propre non nulle du laplacien normalisé.

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

The spectrum of a graph

Equations

• G.lapSpectrum = spectrum ℝ UnweightedGraph.Laplacian

@[reducible, inline]

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

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

Equations

• UnweightedGraph.τ x✝ = 1

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

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

theorem UnweightedGraph.zero_eigenvalue_normalized {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [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 UnweightedGraph.hGH {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] : Laplacian.IsHermitian

Equations

• ⋯ = ⋯

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

Helper to access the eigenvalues by non-decreasing order.

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

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

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

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

The equality in eigval_sum_le_n holds iff G has NoIsolation.

theorem UnweightedGraph.zero_mem_lapSpectrum {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] {G : UnweightedGraph α β} [DecidableRel G.Adj] [OfNat (Fin (Fintype.card α)) 1] [OfNat (Fin (Fintype.card α)) 0] [Nonempty α] (hS : IsSimple) (hLoopless : ∀ (v : α), ¬G.Adj v v) : 0 ∈ G.lapSpectrum

When the graph is non empty, 0 is an eigenvalue of the Laplacian.

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

λ₀ = 0.

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

Second eigenvalue is at most n / n-1.