add_posSemidef — Mathlib

English

If A is positive definite and B is positive semidefinite, then A+B is positive definite.

Русский

Если A положительно определена, а B положительно полуопределена, то A+B положительно определена.

LaTeX

$$$$ \\operatorname{PosDef}(A) \\to \\operatorname{PosSemidef}(B) \\to \\operatorname{PosDef}(A+B). $$$$

Lean4

protected theorem add_posSemidef [AddLeftMono R] {A : Matrix m m R} {B : Matrix m m R} (hA : A.PosDef)
    (hB : B.PosSemidef) : (A + B).PosDef :=
  ⟨hA.isHermitian.add hB.isHermitian, fun x hx =>
    by
    rw [add_mulVec, dotProduct_add]
    exact add_pos_of_pos_of_nonneg (hA.2 x hx) (hB.2 x)⟩

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