Laplacian Matrix

This module defines the Laplacian matrix of a graph, and proves some of its elementary properties.

Main definitions & Results

• SimpleGraph.degMatrix: The degree matrix of a simple graph
• SimpleGraph.lapMatrix: The Laplacian matrix of a simple graph, defined as the difference between the degree matrix and the adjacency matrix.
• isPosSemidef_lapMatrix: The Laplacian matrix is positive semidefinite.
• rank_ker_lapMatrix_eq_card_ConnectedComponent: The number of connected components in G is the dimension of the nullspace of its Laplacian matrix.

def SimpleGraph.degMatrix {V : Type u_1} (α : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [AddMonoidWithOne α] : Matrix V V α

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

Equations

• SimpleGraph.degMatrix α G = Matrix.diagonal fun (x : V) => ↑(SimpleGraph.degree G x)

def SimpleGraph.lapMatrix {V : Type u_1} (α : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [AddGroupWithOne α] : Matrix V V α

lapMatrix G R is the matrix L = D - A where Dis the degree and A the adjacency matrix of G.

Equations

• SimpleGraph.lapMatrix α G = SimpleGraph.degMatrix α G - SimpleGraph.adjMatrix α G

theorem SimpleGraph.isSymm_degMatrix {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [AddMonoidWithOne α] : Matrix.IsSymm (SimpleGraph.degMatrix α G)

theorem SimpleGraph.isSymm_lapMatrix {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [AddGroupWithOne α] : Matrix.IsSymm (SimpleGraph.lapMatrix α G)

theorem SimpleGraph.degMatrix_mulVec_apply {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [NonAssocSemiring α] (v : V) (vec : V → α) : Matrix.mulVec (SimpleGraph.degMatrix α G) vec v = ↑(SimpleGraph.degree G v) * vec v

theorem SimpleGraph.lapMatrix_mulVec_apply {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [NonAssocRing α] (v : V) (vec : V → α) : Matrix.mulVec (SimpleGraph.lapMatrix α G) vec v = ↑(SimpleGraph.degree G v) * vec v - Finset.sum (SimpleGraph.neighborFinset G v) fun (u : V) => vec u

theorem SimpleGraph.lapMatrix_mulVec_const_eq_zero {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Ring α] : (Matrix.mulVec (SimpleGraph.lapMatrix α G) fun (x : V) => 1) = 0

theorem SimpleGraph.dotProduct_mulVec_degMatrix {V : Type u_1} {α : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [CommRing α] (x : V → α) : Matrix.dotProduct x (Matrix.mulVec (SimpleGraph.degMatrix α G) x) = Finset.sum Finset.univ fun (i : V) => ↑(SimpleGraph.degree G i) * x i * x i

theorem SimpleGraph.degree_eq_sum_if_adj {V : Type u_1} (α : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [AddCommMonoidWithOne α] (i : V) : ↑(SimpleGraph.degree G i) = Finset.sum Finset.univ fun (j : V) => if G.Adj i j then 1 else 0

theorem SimpleGraph.lapMatrix_toLinearMap₂' {V : Type u_1} (α : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Field α] [CharZero α] (x : V → α) : ((Matrix.toLinearMap₂' (SimpleGraph.lapMatrix α G)) x) x = (Finset.sum Finset.univ fun (i : V) => Finset.sum Finset.univ fun (j : V) => if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Let $L$ be the graph Laplacian and let $x \in \mathbb{R}$, then $$x^{\top} L x = \sum_{i \sim j} (x_{i}-x_{j})^{2}$$, where $\sim$ denotes the adjacency relation

theorem SimpleGraph.posSemidef_lapMatrix {V : Type u_1} (α : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrderedField α] [StarOrderedRing α] [TrivialStar α] : Matrix.PosSemidef (SimpleGraph.lapMatrix α G)

The Laplacian matrix is positive semidefinite

theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj {V : Type u_1} (α : Type u_2) [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [LinearOrderedField α] (x : V → α) : ((Matrix.toLinearMap₂' (SimpleGraph.lapMatrix α G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j

theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j

theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : ((Matrix.toLinearMap₂' (SimpleGraph.lapMatrix ℝ G)) x) x = 0 ↔ ∀ (i j : V), SimpleGraph.Reachable G i j → x i = x j

theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (x : V → ℝ) : (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), SimpleGraph.Reachable G i j → x i = x j

theorem SimpleGraph.mem_ker_toLin'_lapMatrix_of_connectedComponent {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] (c : SimpleGraph.ConnectedComponent G) : (fun (i : V) => if SimpleGraph.connectedComponentMk G i = c then 1 else 0) ∈ LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G))

def SimpleGraph.lapMatrix_ker_basis_aux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] (c : SimpleGraph.ConnectedComponent G) : ↥(LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)))

Given a connected component c of a graph G, lapMatrix_ker_basis_aux c is the map V → ℝ which is 1 on the vertices in c and 0 elsewhere. The family of these maps indexed by the connected components of G proves to be a basis of the kernel of lapMatrix G R

Equations

• SimpleGraph.lapMatrix_ker_basis_aux G c = { val := fun (i : V) => if SimpleGraph.connectedComponentMk G i = c then 1 else 0, property := ⋯ }

theorem SimpleGraph.linearIndependent_lapMatrix_ker_basis_aux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] : LinearIndependent ℝ (SimpleGraph.lapMatrix_ker_basis_aux G)

theorem SimpleGraph.top_le_span_range_lapMatrix_ker_basis_aux {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] : ⊤ ≤ Submodule.span ℝ (Set.range (SimpleGraph.lapMatrix_ker_basis_aux G))

noncomputable def SimpleGraph.lapMatrix_ker_basis {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] : Basis (SimpleGraph.ConnectedComponent G) ℝ ↥(LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)))

lapMatrix_ker_basis G is a basis of the nullspace indexed by its connected components, the basis is made up of the functions V → ℝ which are 1 on the vertices of the given connected component and 0 elsewhere.

Equations

• SimpleGraph.lapMatrix_ker_basis G = Basis.mk ⋯ ⋯

theorem SimpleGraph.card_ConnectedComponent_eq_rank_ker_lapMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq (SimpleGraph.ConnectedComponent G)] : Fintype.card (SimpleGraph.ConnectedComponent G) = FiniteDimensional.finrank ℝ ↥(LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)))

The number of connected components in G is the dimension of the nullspace its Laplacian.