re_dotProduct_nonneg — Mathlib

English

For any x, the real part of x* M x is nonnegative when M is PSD.

Русский

Для любого вектора x действительная часть скалярного произведения x* M x неотрицательна, если M является PSD.

LaTeX

$$$0 \le \operatorname{Re}(x^* M x) \quad (M \text{ PSD})$$

Lean4

theorem re_dotProduct_nonneg {M : Matrix n n 𝕜} (hM : M.PosSemidef) (x : n → 𝕜) : 0 ≤ RCLike.re (star x ⬝ᵥ (M *ᵥ x)) :=
  RCLike.nonneg_iff.mp (hM.2 _) |>.1

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