English
Let M be positive definite. Then the space of all n×n matrices, with the inner product ⟨X,Y⟩_M = tr(Y M X^*), becomes a complex inner product space; this induces a norm, turning M_n(𝕜) into a NormedAddCommGroup.
Русский
Пусть M положительно определена. Тогда пространство всех матриц размерности n×n, снабжённое скалярным произведением ⟨X,Y⟩_M = tr(Y M X^*), становится комплексным пространством с внутренним произведением; это порождает норму, превращая M_n(𝕜) в нормированную аддитивную группу.
LaTeX
$$$\langle X,Y\rangle_M = \operatorname{tr}(Y M X^*)$ определяет внутреннее произведение на $M_n(\mathbb{K})$ для $M \ PosDef$, и порождает норму.$$
Lean4
/-- A positive definite matrix `M` induces a norm on `Matrix n n 𝕜`:
`‖x‖ = sqrt (x * M * xᴴ).trace`. -/
noncomputable def matrixNormedAddCommGroup {M : Matrix n n 𝕜} (hM : M.PosDef) : NormedAddCommGroup (Matrix n n 𝕜) :=
letI : InnerProductSpace.Core 𝕜 (Matrix n n 𝕜) :=
{ inner x y := (y * M * xᴴ).trace
conj_inner_symm _
_ := by
simp only [mul_assoc, starRingEnd_apply, ← trace_conjTranspose, conjTranspose_mul, conjTranspose_conjTranspose,
hM.isHermitian.eq]
re_inner_nonneg x := RCLike.nonneg_iff.mp (hM.posSemidef.mul_mul_conjTranspose_same x).trace_nonneg |>.1
add_left := by simp [mul_add]
smul_left := by simp
definite x
hx := by
classical
obtain ⟨y, hy, rfl⟩ := Matrix.posDef_iff_eq_conjTranspose_mul_self.mp hM
rw [← mul_assoc, ← conjTranspose_conjTranspose x, ← conjTranspose_mul, conjTranspose_conjTranspose, mul_assoc,
trace_conjTranspose_mul_self_eq_zero_iff] at hx
lift y to (Matrix n n 𝕜)ˣ using hy
simpa [← mul_assoc] using congr(y⁻¹ * $hx) }
this.toNormedAddCommGroup
