lapMatrix_mulVec_apply — Mathlib

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]

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