English
Reiterates the identity xᵀ (DegMatrix) x = ∑ deg(i) x_i^2.
Русский
Повторяет тождество: xᵀ (DegMatrix) x = ∑ deg(i) x_i^2.
LaTeX
$$$x \cdot (G.degMatrix R \cdot x) = \sum_{i} G.degree(i) x(i)^2$$$
Lean4
/-- The Laplacian matrix is positive semidefinite -/
theorem posSemidef_lapMatrix [Field R] [LinearOrder R] [IsStrictOrderedRing R] [StarRing R] [TrivialStar R] :
PosSemidef (G.lapMatrix R) := by
constructor
· rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]
· intro x
rw [star_trivial, ← toLinearMap₂'_apply', lapMatrix_toLinearMap₂']
positivity