Documentation

Mathlib.Combinatorics.SimpleGraph.LapMatrix

Laplacian Matrix #

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

Main definitions & Results #

theorem SimpleGraph.degree_eq_sum_if_adj {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {R : Type u_3} [AddCommMonoidWithOne R] (i : V) :
(G.degree i) = j : V, if G.Adj i j then 1 else 0
def SimpleGraph.degMatrix {V : Type u_1} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [AddMonoidWithOne R] :
Matrix V V R

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

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

The Laplacian matrix lapMatrix G R of a graph G is the matrix L = D - A where D is the degree and A the adjacency matrix of G.

Equations
theorem SimpleGraph.degMatrix_mulVec_apply {V : Type u_1} {R : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [NonAssocSemiring R] (v : V) (vec : VR) :
(degMatrix R G).mulVec vec v = (G.degree v) * vec v
theorem SimpleGraph.lapMatrix_mulVec_apply {V : Type u_1} {R : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [NonAssocRing R] (v : V) (vec : VR) :
(lapMatrix R G).mulVec vec v = (G.degree v) * vec v - uG.neighborFinset v, vec u
theorem SimpleGraph.lapMatrix_mulVec_const_eq_zero {V : Type u_1} {R : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [NonAssocRing R] :
((lapMatrix R G).mulVec fun (x : V) => 1) = 0
theorem SimpleGraph.dotProduct_mulVec_degMatrix {V : Type u_1} {R : Type u_2} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [CommSemiring R] (x : VR) :
x ⬝ᵥ (degMatrix R G).mulVec x = i : V, (G.degree i) * x i * x i
theorem SimpleGraph.lapMatrix_toLinearMap₂' {V : Type u_1} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [Field R] [CharZero R] (x : VR) :
(((Matrix.toLinearMap₂' R) (lapMatrix R G)) x) x = (∑ i : V, j : V, if G.Adj i j then (x i - x j) ^ 2 else 0) / 2

Let L be the graph Laplacian and let xR, then xLx=ij(xixj)2, where denotes the adjacency relation

The Laplacian matrix is positive semidefinite

theorem SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj {V : Type u_1} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] (x : VR) :
(((Matrix.toLinearMap₂' R) (lapMatrix R G)) x) x = 0 ∀ (i j : V), G.Adj i jx i = x j
theorem SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] {x : V} :
(lapMatrix G).mulVec x = 0 ∀ (i j : V), G.Adj i jx i = x j
@[deprecated SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_adj (since := "2025-05-18")]
theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_adj {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (x : V) :
(Matrix.toLin' (lapMatrix G)) x = 0 ∀ (i j : V), G.Adj i jx i = x j
theorem SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] {x : V} :
(lapMatrix G).mulVec x = 0 ∀ (i j : V), G.Reachable i jx i = x j
@[deprecated SimpleGraph.lapMatrix_mulVec_eq_zero_iff_forall_reachable (since := "2025-05-18")]
theorem SimpleGraph.lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] (x : V) :
(Matrix.toLin' (lapMatrix G)) x = 0 ∀ (i j : V), G.Reachable i jx i = x j

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

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

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

@[deprecated SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix (since := "2025-04-29")]

Alias of SimpleGraph.card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix.


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