nonneg

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.PosDef.nonneg

← MathLib Explorer

English

If Q is PosDef, then Q x ≥ 0 for all x.

Русский

Если Q положительно определена, то Q x неотрицательно для всякого x.

LaTeX

$$$\\mathrm{PosDef}(Q) \\Rightarrow \\forall x, 0 \\le Q(x).$$$

Lean4

theorem nonneg {Q : QuadraticMap R₂ M N} (hQ : PosDef Q) (x : M) : 0 ≤ Q x :=
  (eq_or_ne x 0).elim (fun h => h.symm ▸ (map_zero Q).symm.le) fun h => (hQ _ h).le

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru