English
Let G be a finite graph on vertex set V and let L be its Laplacian matrix L = lapMatrix ℝ G. For any x: V → ℝ, the quadratic form x^T L x equals 0 if and only if x_i = x_j for all i, j that are connected by a path in G (i.e., G.Reachable i j). Equivalently, x is constant on every connected component of G.
Русский
Пусть G — конечный граф на множестве вершин V, а L — его лапласиан. Для любого x: V → ℝ крестовая форма x^T L x равна 0 тогда и только тогда, когда x_i = x_j для всех i, j, связанных по пути в G (то есть G.Reachable i j). Эквивалентно: x константен на каждой связной компоненте G.
LaTeX
$$$$ x^\\top (G.lapMatrix \\mathbb{R}) x = 0 \\iff \\forall i,j \\in V,\\ G.Reachable i j \\to x_i = x_j. $$$$
Lean4
theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable (x : V → ℝ) :
Matrix.toLinearMap₂' ℝ (G.lapMatrix ℝ) x x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j :=
by
rw [lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj]
refine ⟨?_, fun h i j hA ↦ h i j hA.reachable⟩
intro h i j ⟨w⟩
induction w with
| nil => rfl
| cons hA _ h' => exact (h _ _ hA).trans h'
