lapMatrix_mulVec_eq_zero_iff_forall_reachable

English

For a finite graph G with Laplacian L, a vector x: V → ℝ satisfies L x = 0 if and only if x is constant on every connected component of G; equivalently, x_i = x_j whenever i and j are reachable from each other.

Русский

Для конечного графа G с лапласианом L верно: Lx = 0 тогда и только тогда, когда x константен на каждой связной компоненте G; то есть x_i = x_j, если i и j достижимы друг от друга.

LaTeX

$$$$ (G.lapMatrix \\mathbb{R}) x = 0 \\iff \\forall i,j \\in V,\\ G.Reachable i j \\to x_i = x_j. $$$$

Lean4

theorem lapMatrix_mulVec_eq_zero_iff_forall_reachable {x : V → ℝ} :
    G.lapMatrix ℝ *ᵥ x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j := by
  rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
    lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]

Похожие утверждения