conjTranspose_mul_mul_same — Mathlib

English

If A is PSD, then B* A B is PSD for any B.

Русский

Если A положительно полуопределена, то B* A B положительно полуопределена для всякой матрицы B.

LaTeX

$$$A \succeq 0 \Rightarrow B^* A B \succeq 0$$$

Lean4

theorem conjTranspose_mul_mul_same {A : Matrix n n R} (hA : PosSemidef A) {m : Type*} [Fintype m] (B : Matrix n m R) :
    PosSemidef (Bᴴ * A * B) := by
  constructor
  · exact isHermitian_conjTranspose_mul_mul B hA.1
  · intro x
    simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.2 (B *ᵥ x)

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