posSemidef_conjTranspose_mul_self

English

For any A, the Gram matrix AᴴA is positive semidefinite.

Русский

Для любого A матрица G = AᴴA является положительной полуопределенной.

LaTeX

$$$A^\!\!H A \succeq 0$$$

Lean4

/-- The conjugate transpose of a matrix multiplied by the matrix is positive semidefinite -/
theorem posSemidef_conjTranspose_mul_self [StarOrderedRing R] (A : Matrix m n R) : PosSemidef (Aᴴ * A) :=
  by
  refine ⟨isHermitian_transpose_mul_self _, fun x => ?_⟩
  rw [← mulVec_mulVec, dotProduct_mulVec, vecMul_conjTranspose, star_star]
  exact Finset.sum_nonneg fun i _ => star_mul_self_nonneg _

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