posDef_of_nonneg — Mathlib

English

If Q is nonnegative on all inputs and Q is anisotropic, then Q is positive definite.

Русский

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

LaTeX

$$$\big( \forall x, Q(x) \ge 0 \big) \land Q \text{ Anisotropic} \Rightarrow \operatorname{PosDef}(Q)$$$

Lean4

theorem posDef_of_nonneg {Q : QuadraticMap R₂ M N} (h : ∀ x, 0 ≤ Q x) (h0 : Q.Anisotropic) : PosDef Q := fun x hx =>
  lt_of_le_of_ne (h x) (Ne.symm fun hQx => hx <| h0 _ hQx)

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