English
Let M be a positive definite matrix in M_n(𝕜). Then the bilinear form on the space of n-by-n matrices defined by ⟨X,Y⟩_M := tr(Y M X^H) is an inner product, turning M_n(𝕜) into an inner product space over 𝕜.
Русский
Пусть M — положительно определённая матрица из M_n(𝕜). Тогда билинейная форма ⟨X,Y⟩_M := tr(Y M X^H) на пространстве матриц n×n задаёт скалярное произведение, и пространство матриц M_n(𝕜) становится скалярным произведением над 𝕜.
LaTeX
$$$\text{Пусть } M \in M_n(\mathbb{K})\text{ положительно определена. Тогда } \langle X,Y\rangle_M := \operatorname{tr}(Y M X^H) \text{ задаёт скалярное произведение на } M_n(\mathbb{K}).$$$
Lean4
/-- A positive definite matrix `M` induces an inner product on `Matrix n n 𝕜`:
`⟪x, y⟫ = (y * M * xᴴ).trace`. -/
def matrixInnerProductSpace {M : Matrix n n 𝕜} (hM : M.PosDef) :
letI : NormedAddCommGroup (Matrix n n 𝕜) := hM.matrixNormedAddCommGroup
InnerProductSpace 𝕜 (Matrix n n 𝕜) :=
InnerProductSpace.ofCore _
