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.
• posSemidef_lapMatrix: The Laplacian matrix is positive semidefinite.
• card_connectedComponent_eq_finrank_ker_toLin'_lapMatrix: The number of connected components in a graph is the dimension of the nullspace of its Laplacian matrix.

@[simp]

theorem Matrix.IsAdjMatrix.isHermitian {α : Type u_1} {V : Type u_2} [NonAssocSemiring α] [StarRing α] {A : Matrix V V α} (h : A.IsAdjMatrix) : A.IsHermitian

theorem SimpleGraph.isHermitian_adjMatrix {V : Type u_1} (R : Type u_2) (G : SimpleGraph V) [DecidableRel G.Adj] [NonAssocSemiring R] [StarRing R] : (adjMatrix R G).IsHermitian

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

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

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

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

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

theorem SimpleGraph.isHermitian_degMatrix {V : Type u_1} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [NonAssocSemiring R] [StarRing R] : (degMatrix R G).IsHermitian

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

theorem SimpleGraph.isHermitian_lapMatrix {V : Type u_1} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [NonAssocRing R] [StarRing R] : (lapMatrix R G).IsHermitian

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 : V → R) : (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 : V → R) : (lapMatrix R G).mulVec vec v = ↑(G.degree v) * vec v - ∑ u ∈ G.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 : V → R) : 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 : V → R) : (((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 $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} (R : Type u_2) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [StarRing R] [TrivialStar R] : (lapMatrix R G).PosSemidef

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 : V → R) : (((Matrix.toLinearMap₂' R) (lapMatrix R G)) x) x = 0 ↔ ∀ (i j : V), G.Adj i j → x 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 j → x i = x j

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

@[simp]

theorem SimpleGraph.det_lapMatrix_eq_zero {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [h : Nonempty V] : (lapMatrix ℝ G).det = 0

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) ∈ (Matrix.toLin' (lapMatrix ℝ G)).ker

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

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] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [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] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] [DecidableEq G.ConnectedComponent] : ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

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

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 = Module.Basis.mk ⋯ ⋯

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

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