submatrix — Mathlib

English

If M is PSD, then the submatrix M[e,e] is PSD for any index map e.

Русский

Если M — ПСД, то подматрица M[e,e] по любому отображению индексов e также ПСД.

LaTeX

$$$M \text{ PosSemidef} \Rightarrow M_{e,e} \text{ PosSemidef}$$$

Lean4

theorem submatrix {M : Matrix n n R} (hM : M.PosSemidef) (e : m → n) : (M.submatrix e e).PosSemidef := by
  classical
  rw [(by simp : M = 1 * M * 1), submatrix_mul (he₂ := Function.bijective_id),
    submatrix_mul (he₂ := Function.bijective_id), submatrix_id_id]
  simpa only [conjTranspose_submatrix, conjTranspose_one] using conjTranspose_mul_mul_same hM (Matrix.submatrix 1 id e)

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