posDef_iff_nonneg — Mathlib

English

A quadratic map Q is positive definite if and only if Q is nonnegative on all inputs and anisotropic.

Русский

Квадратичная карта Q положительно определена тогда и только тогда, когда она неотрицательна на всех входах и анизотропна.

LaTeX

$$$\operatorname{PosDef}(Q) \iff \big( \forall x, 0 \le Q(x) \big) \land \operatorname{Anisotropic}(Q)$$$

Lean4

theorem posDef_iff_nonneg {Q : QuadraticMap R₂ M N} : PosDef Q ↔ (∀ x, 0 ≤ Q x) ∧ Q.Anisotropic :=
  ⟨fun h => ⟨h.nonneg, h.anisotropic⟩, fun ⟨n, a⟩ => posDef_of_nonneg n a⟩

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