of_toQuadraticForm' — Mathlib

English

If a matrix M is symmetric and its associated quadratic form is positive definite, then M is positive definite.

Русский

Если матрица M симметрична, и связанная с ней квадратичная форма положительно определена, то M тоже положительно определена.

LaTeX

$$$$ M \\text{IsSymm} \\land M.toQuadraticMap'.PosDef \\Rightarrow M.PosDef. $$$$

Lean4

theorem of_toQuadraticForm' [DecidableEq n] {M : Matrix n n ℝ} (hM : M.IsSymm) (hMq : M.toQuadraticMap'.PosDef) :
    M.PosDef := by
  refine ⟨hM, fun x hx => ?_⟩
  simp only [toQuadraticMap', QuadraticMap.PosDef, LinearMap.BilinMap.toQuadraticMap_apply, toLinearMap₂'_apply'] at hMq
  apply hMq x hx

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