dotProduct_mulVec_degMatrix — Mathlib

English

The dot product xᵀ with (degMatrix R G) x equals sum over i of deg(i)·x_i^2.

Русский

Пусть x — вектор; тогда xᵀ D x = ∑_i deg(i) x_i^2.

LaTeX

$$$x \cdot (G.degMatrix R \cdot x) = \sum_{i \in V} G.degree(i) \cdot x(i)^2$$$

Lean4

theorem dotProduct_mulVec_degMatrix [CommSemiring R] (x : V → R) :
    x ⬝ᵥ (G.degMatrix R *ᵥ x) = ∑ i : V, G.degree i * x i * x i := by
  simp only [dotProduct, degMatrix, mulVec_diagonal, ← mul_assoc, mul_comm]

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