pow — Mathlib

English

If M is PSD, then M^k is PSD for any natural k.

Русский

Если M ПСД, то M^k ПСД для любого натурального k.

LaTeX

$$$M^k \text{ PSD for all } k \in \mathbb{N}$ given $M \succeq 0$$$

Lean4

protected theorem pow [StarOrderedRing R] [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) (k : ℕ) :
    PosSemidef (M ^ k) :=
  match k with
  | 0 => .one
  | 1 => by simpa using hM
  | (k + 2) => by
    rw [pow_succ, pow_succ']
    simpa only [hM.isHermitian.eq] using (hM.pow k).mul_mul_conjTranspose_same M

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