lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj

English

The linear map derived from the Laplacian equals zero exactly when all adjacent vertices have equal values, i.e., x_i = x_j for all adjacent i,j.

Русский

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

LaTeX

$$$\text{toLinearMap}_2'\ R (G.lapMatrix R) x x = 0 \iff \forall i j, G.Adj i j \Rightarrow x_i = x_j$$$

Lean4

theorem lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_adj [Field R] [LinearOrder R] [IsStrictOrderedRing R]
    (x : V → R) : Matrix.toLinearMap₂' R (G.lapMatrix R) x x = 0 ↔ ∀ i j : V, G.Adj i j → x i = x j := by
  simp (disch := intros; positivity) [lapMatrix_toLinearMap₂', sum_eq_zero_iff_of_nonneg, sub_eq_zero]

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