jd_transform — Mathlib

English

The identity (PD)ᵀ · JD · PD = 2 · S holds, linking JD, PD, and S via a bilinear form.

Русский

Имеется тождество (PD)ᵀ · JD · PD = 2 · S, связывающее JD, PD и S через билинейную форму.

LaTeX

$$$ (PD(l,R))^{\top} \cdot JD(l,R) \cdot PD(l,R) = 2 \cdot S(l,R). $$$

Lean4

theorem jd_transform [Fintype l] : (PD l R)ᵀ * JD l R * PD l R = (2 : R) • S l R :=
  by
  have h : (PD l R)ᵀ * JD l R = Matrix.fromBlocks 1 1 1 (-1) := by
    simp [PD, JD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply]
  rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
  simp [two_smul]

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