lapMatrix_mulVec_eq_zero_iff_forall_adj

English

The Laplacian times vector x equals zero if and only if x is constant on every edge-connected pair: for all i,j with G.Adj i j, x_i = x_j.

Русский

Умножение лапласиана на вектор x равно нулю тогда, когда на любом ребре значения вершин совпадают: для всех i,j, если G.Adj i j, то x_i = x_j.

LaTeX

$$$G.lapMatrix Real G \cdot x = 0 \iff \forall i j, G.Adj i j \Rightarrow x_i = x_j$$$

Lean4

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

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