add — Mathlib

English

If Q and Q' are positive definite, then their sum Q+Q' is positive definite (under appropriate monotonicity assumptions).

Русский

Если Q и Q' положительно определены, то их сумма Q+Q' также положительно определена (при разумных предпосылках монотонности).

LaTeX

$$$\operatorname{PosDef}(Q) \land \operatorname{PosDef}(Q') \Rightarrow \operatorname{PosDef}(Q+Q')$$$

Lean4

theorem add [AddLeftStrictMono N] (Q Q' : QuadraticMap R₂ M N) (hQ : PosDef Q) (hQ' : PosDef Q') : PosDef (Q + Q') :=
  fun x hx => add_pos (hQ x hx) (hQ' x hx)

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