English
Let M be a positive definite matrix. Then on the vector space of n-tuples over 𝕜, one gets an inner product ⟪x, y⟫_M = x* M y, which induces a norm ‖x‖_M = sqrt(Re ⟪x, x⟫_M). In particular, this defines a normed inner product space with norm coming from M.
Русский
Пусть M — положительно определенная матрица. Тогда на пространстве векторов 𝕜^n задаётся скалярное произведение ⟪x, y⟫_M = x^* M y, порождающее норму ‖x‖_M = sqrt(Re ⟪x, x⟫_M). Это задаёт нормированное скалярное произведение и соответствующую норму.
LaTeX
$$$\langle x,y\rangle_M = x^* M y,\quad \|x\|_M^2 = \operatorname{Re}\langle x,x\rangle_M.$$$
Lean4
/-- A positive definite matrix `M` induces a norm `‖x‖ = sqrt (re xᴴMx)`. -/
noncomputable abbrev ofMatrix {M : Matrix n n 𝕜} (hM : M.PosDef) : NormedAddCommGroup (n → 𝕜) :=
@InnerProductSpace.Core.toNormedAddCommGroup _ _ _ _ _
{ inner x y := (M *ᵥ y) ⬝ᵥ star x
conj_inner_symm x
y := by
rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star, star_mulVec, dotProduct_comm (M *ᵥ y),
dotProduct_mulVec, hM.isHermitian.eq]
re_inner_nonneg x := dotProduct_comm _ (star x) ▸ hM.posSemidef.re_dotProduct_nonneg x
definite x
(hx : _ ⬝ᵥ _ = 0) := by
by_contra! h
simpa [hx, lt_irrefl, dotProduct_comm] using hM.re_dotProduct_pos h
add_left := by simp only [star_add, dotProduct_add, forall_const]
smul_left _ _ _ := by rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul] }
