WeightedGraph

This file develops the basic theory of weighted multigraphs WeightedGraph α β.

Main definitions

• WeightedGraph is a finite Graph associated with a weight function.
• degreeMatrix and lapMatrix: matrices associated with a graph.

References

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

structure WeightedGraph (α : Type u_4) (β : Type u_5) (K : Type u_6) extends Graph α β : Type (max (max u_4 u_5) u_6)

A weighted multigraph on types α β K is a Graph α β associated with a function w: β → K.

• 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
• w : β → K

Finiteness at a vertex

This section deals with vertices that have finitely many adjacent vertices. We denote this condition by Fintype (G.incidenceSet v). We define G.neighborFinset v to be the Finset version of G.neighborSet v.

def WeightedGraph.incidenceFinset {α : Type u_1} {β : Type u_2} {K : Type u_3} (G : WeightedGraph α β K) (v : α) [Fintype ↑(Graph.incidenceSet v)] : Finset β

G.incidenceFinset v is the Finset version of G.incidenceSet v in case G is locally finite at v.

Equations

• G.incidenceFinset v = (Graph.incidenceSet v).toFinset

def WeightedGraph.degree {α : Type u_1} {β : Type u_2} {K : Type u_3} (G : WeightedGraph α β K) [AddCommMonoid K] (v : α) [Fintype ↑(Graph.incidenceSet v)] : K

The degree of v in G is the sum of G.w e for every edge e linked to v.

Equations

• G.degree v = ∑ e ∈ G.incidenceFinset v, G.w e

def WeightedGraph.linkWeight {α : Type u_1} {β : Type u_2} {K : Type u_3} (G : WeightedGraph α β K) [AddCommMonoid K] (u v : α) [Fintype ↑(Graph.incidenceSet u)] [(e : β) → (u v : α) → Decidable (G.IsLink e u v)] : K

The total weight of edges linking u and v.

Equations

• G.linkWeight u v = ∑ e ∈ G.incidenceFinset u, if G.IsLink e u v then G.w e else 0

theorem WeightedGraph.weight_comm {α : Type u_1} {β : Type u_2} {K : Type u_3} (G : WeightedGraph α β K) [AddCommMonoid K] (u v : α) [Fintype ↑(Graph.incidenceSet v)] [Fintype ↑(Graph.incidenceSet u)] [(e : β) → (u v : α) → Decidable (G.IsLink e u v)] : G.linkWeight u v = G.linkWeight v u

Symmetry of edge weight between two vertices.

Finite Graph

This section states results about graphs with a finite number of vertices and edges.

def WeightedGraph.vol {α : Type u_1} {β : Type u_2} {K : Type u_3} (G : WeightedGraph α β K) [AddCommMonoid K] [(u : α) → Fintype ↑(Graph.incidenceSet u)] [Fintype ↑G.vertexSet] : K

The volume of a graph G is the sum of the degrees of its vertices.

Equations

• G.vol = ∑ u : ↑G.vertexSet, G.degree ↑u

Finite Graph

This section states results about graphs associated with a real weight function.

def WeightedGraph.degreeMatrix {α : Type u_1} {β : Type u_2} (G : WeightedGraph α β ℝ) [(u : α) → Fintype ↑(Graph.incidenceSet u)] [DecidableEq ↑G.vertexSet] : Matrix ↑G.vertexSet ↑G.vertexSet ℝ

The diagonal matrix consisting of the degrees of the vertices in the graph.

Equations

• G.degreeMatrix = Matrix.diagonal fun (u : ↑G.vertexSet) => G.degree ↑u

noncomputable def WeightedGraph.lapMatrix {α : Type u_1} {β : Type u_2} (G : WeightedGraph α β ℝ) [(u : α) → Fintype ↑(Graph.incidenceSet u)] [DecidableEq ↑G.vertexSet] [(e : β) → (u v : α) → Decidable (G.IsLink e u v)] [DecidableRel G.Adj] : Matrix ↑G.vertexSet ↑G.vertexSet ℝ

The Laplacian matrix lapMatrix of a weighted graph G.

Equations

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

theorem WeightedGraph.isHermitian_lapMatrix {α : Type u_1} {β : Type u_2} (G : WeightedGraph α β ℝ) [(u : α) → Fintype ↑(Graph.incidenceSet u)] [DecidableEq ↑G.vertexSet] [(e : β) → (u v : α) → Decidable (G.IsLink e u v)] [DecidableRel G.Adj] : G.lapMatrix.IsHermitian

noncomputable def WeightedGraph.lapEigvals {α : Type u_1} {β : Type u_2} (G : WeightedGraph α β ℝ) [(u : α) → Fintype ↑(Graph.incidenceSet u)] [DecidableEq ↑G.vertexSet] [(e : β) → (u v : α) → Decidable (G.IsLink e u v)] [DecidableRel G.Adj] [Fintype ↑G.vertexSet] : Fin (Fintype.card ↑G.vertexSet) → ℝ

Eigenvalues of lapMatrix in non-increasing order.

Equations

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