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) => ↑(G.degree 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 α] : (SimpleGraph.degMatrix α G).IsSymm

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

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 → α) : (SimpleGraph.degMatrix α G).mulVec vec v = ↑(G.degree 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 → α) : (SimpleGraph.lapMatrix α G).mulVec vec v = ↑(G.degree v) * vec v - (G.neighborFinset v).sum 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 α] : ((SimpleGraph.lapMatrix α G).mulVec 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 ((SimpleGraph.degMatrix α G).mulVec x) = Finset.univ.sum fun (i : V) => ↑(G.degree 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) : ↑(G.degree i) = Finset.univ.sum 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.univ.sum fun (i : V) => Finset.univ.sum 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 α] [StarRing α] [StarOrderedRing α] [TrivialStar α] : (SimpleGraph.lapMatrix α G).PosSemidef

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), G.Reachable 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), G.Reachable 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 G.ConnectedComponent] (c : G.ConnectedComponent) : (fun (i : V) => if G.connectedComponentMk 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 G.ConnectedComponent] (c : G.ConnectedComponent) : ↥(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

• G.lapMatrix_ker_basis_aux c = ⟨fun (i : V) => if G.connectedComponentMk i = c then 1 else 0, ⋯⟩

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

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 G.ConnectedComponent] : ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

noncomputable def SimpleGraph.lapMatrix_ker_basis {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq G.ConnectedComponent] : Basis G.ConnectedComponent ℝ ↥(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

• G.lapMatrix_ker_basis = 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 G.ConnectedComponent] : Fintype.card G.ConnectedComponent = FiniteDimensional.finrank ℝ ↥(LinearMap.ker (Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)))

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