English
The Laplacian acting on vec yields a vector with i-th component equal to deg(i)·vec(i) minus the sum of vec over neighbors of i.
Русский
Лапласиан действует на vec и даёт в i-й компоненте deg(i)·vec(i) минус сумму vec по соседям i.
LaTeX
$$$(G.lapMatrix R *\! vec)_v = G.degree(v) * vec(v) - \sum_{u \in G.neighborFinset v} vec(u)$$$
Lean4
theorem lapMatrix_mulVec_apply [NonAssocRing R] (v : V) (vec : V → R) :
(G.lapMatrix R *ᵥ vec) v = G.degree v * vec v - ∑ u ∈ G.neighborFinset v, vec u := by
simp_rw [lapMatrix, sub_mulVec, Pi.sub_apply, degMatrix_mulVec_apply, adjMatrix_mulVec_apply]