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]