dotProduct_mulVec_adjMatrix — Mathlib

English

Let α be a NonAssocSemiring. For vectors x,y : V → α, and A the adjacency matrix of G over α, we have x^T A y = ∑_{i,j} (if G.Adj i j then x_i y_j else 0).

Русский

Пусть α — неассоциативная полугруппа с единицей. Пусть x,y : V → α. Тогда x^T A y = сумма по i,j от (если G.Adj i j тогда x_i y_j, иначе 0), где A — матрица смежности G над α.

LaTeX

$$$ x^\top A y = \sum_{i\in V} \sum_{j\in V} \begin{cases} x_i y_j, & G.Adj(i,j), \\ 0, & \text{иначе}. \end{cases} $$$

Lean4

theorem dotProduct_mulVec_adjMatrix [NonAssocSemiring α] (x y : V → α) :
    x ⬝ᵥ G.adjMatrix α *ᵥ y = ∑ i : V, ∑ j : V, if G.Adj i j then x i * y j else 0 := by
  simp only [dotProduct, mulVec, adjMatrix_apply, ite_mul, one_mul, zero_mul, mul_sum, mul_ite, mul_zero]

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