Problem 6: Large epsilon-light vertex subsets -- Laplacian Basics

Basic definitions: edge Laplacian, graph Laplacian, induced Laplacian, epsilon-lightness. Fundamental properties: PSD, symmetry, equivalence with mathlib's lapMatrix.

Main definitions

• Problem6.graphLaplacian: graph Laplacian as sum of edge Laplacians
• Problem6.inducedLaplacian: Laplacian of the induced subgraph on S
• Problem6.inducedSubgraph: the induced subgraph on S as a SimpleGraph V
• Problem6.IsEpsLight: epsilon-lightness predicate

Main theorems

• Problem6.graphLaplacian_eq_lapMatrix: equivalence with mathlib
• Problem6.graphLaplacian_posSemidef: graph Laplacian is PSD
• Problem6.graphLaplacian_isHermitian: graph Laplacian is symmetric
• Problem6.inducedLaplacian_eq_lapMatrix: inducedLaplacian = (inducedSubgraph G S).lapMatrix ℝ
• Problem6.lapMatrix_loewner_mono: Loewner monotonicity for lapMatrix

def Problem6.graphLaplacian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

The Laplacian matrix of a simple graph, defined as ∑{e ∈ E} L_e where each L_e is the edge Laplacian. We use the standard definition L{ij} = deg(i) if i=j, -1 if i~j, 0 otherwise.

Equations

• Problem6.graphLaplacian G = Matrix.of fun (i j : V) => if i = j then ↑(Finset.filter (G.Adj i) Finset.univ).card else if G.Adj i j then -1 else 0

def Problem6.inducedLaplacian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Matrix V V ℝ

The Laplacian of the induced subgraph on S: restricting to edges within S.

Equations

• Problem6.inducedLaplacian G S = Matrix.of fun (i j : V) => if i = j then ↑{k : V | i ∈ S ∧ k ∈ S ∧ G.Adj i k}.card else if G.Adj i j ∧ i ∈ S ∧ j ∈ S then -1 else 0

def Problem6.IsEpsLight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ε : ℝ) (S : Finset V) : Prop

A set S is ε-light if εL - L_S is positive semidefinite.

Equations

• Problem6.IsEpsLight G ε S = (ε • Problem6.graphLaplacian G - Problem6.inducedLaplacian G S).PosSemidef

The induced subgraph as a SimpleGraph V

Using Mathlib's Subgraph.induce and Subgraph.spanningCoe to construct the induced subgraph on S as a SimpleGraph V, connecting to Mathlib's lapMatrix API.

@[reducible, inline]

noncomputable abbrev Problem6.inducedSubgraph {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : SimpleGraph V

The induced subgraph of G on S, as a SimpleGraph V. Uses Mathlib's Subgraph.induce + spanningCoe to stay in SimpleGraph V.

Equations

• Problem6.inducedSubgraph G S = (⊤.induce ↑S).spanningCoe

@[implicit_reducible]

instance Problem6.inducedSubgraphDecidableRelAdj {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : DecidableRel (inducedSubgraph G S).Adj

Equations

• Problem6.inducedSubgraphDecidableRelAdj G S v w = ⋯.mpr inferInstance

theorem Problem6.inducedSubgraph_adj {V : Type u_1} (G : SimpleGraph V) (S : Finset V) (v w : V) : (inducedSubgraph G S).Adj v w ↔ G.Adj v w ∧ v ∈ S ∧ w ∈ S

Adjacency in the induced subgraph: (inducedSubgraph G S).Adj v w ↔ G.Adj v w ∧ v ∈ S ∧ w ∈ S.

theorem Problem6.inducedSubgraph_le {V : Type u_1} (G : SimpleGraph V) (S : Finset V) : inducedSubgraph G S ≤ G

The induced subgraph is a subgraph of G.

theorem Problem6.inducedSubgraph_mono {V : Type u_1} (G : SimpleGraph V) {S T : Finset V} (hST : S ⊆ T) : inducedSubgraph G S ≤ inducedSubgraph G T

Monotonicity: S ⊆ T implies inducedSubgraph G S ≤ inducedSubgraph G T.

theorem Problem6.inducedLaplacian_eq_graphLaplacian_inducedSubgraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : inducedLaplacian G S = graphLaplacian (inducedSubgraph G S)

Bridge: inducedLaplacian G S = graphLaplacian (inducedSubgraph G S).

theorem Problem6.graphLaplacian_eq_lapMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : graphLaplacian G = SimpleGraph.lapMatrix ℝ G

The graph Laplacian equals the Mathlib lapMatrix (degree minus adjacency).

theorem Problem6.inducedLaplacian_eq_lapMatrix {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : inducedLaplacian G S = SimpleGraph.lapMatrix ℝ (inducedSubgraph G S)

Bridge: inducedLaplacian G S = (inducedSubgraph G S).lapMatrix ℝ.

theorem Problem6.graphLaplacian_posSemidef {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (graphLaplacian G).PosSemidef

The graph Laplacian is positive semidefinite. xᵀLx = ∑_{u~v} (x_u - x_v)² ≥ 0.

theorem Problem6.graphLaplacian_isHermitian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : (graphLaplacian G).IsHermitian

The graph Laplacian is symmetric (L is Hermitian since G.Adj is symmetric).

Loewner monotonicity for lapMatrix

theorem Problem6.lapMatrix_loewner_mono {V : Type u_1} [Fintype V] [DecidableEq V] {H₁ H₂ : SimpleGraph V} [DecidableRel H₁.Adj] [DecidableRel H₂.Adj] (h : H₁ ≤ H₂) : (SimpleGraph.lapMatrix ℝ H₂ - SimpleGraph.lapMatrix ℝ H₁).PosSemidef

Loewner monotonicity for graph Laplacians: if H₁ ≤ H₂ (subgraph ordering), then (H₂.lapMatrix ℝ - H₁.lapMatrix ℝ).PosSemidef. Proof: the difference equals the lapMatrix of the edge-difference graph, which is PSD.