posSemidef_lapMatrix — Mathlib

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

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