mul_mul_conjTranspose_same — Mathlib

English

If A is PosDef and B.mulVec is injective, then B A Bᴴ is PosDef.

Русский

Если A положительно определена и B.mulVec инъективна, то B A Bᴴ положительно определена.

LaTeX

$$$$ \\operatorname{PosDef}(A) \\to \\operatorname{Injective}(B.\\operatorname{vecMul}) \\to \\operatorname{PosDef}(B A B^{\\mathrm{H}}). $$$$

Lean4

theorem mul_mul_conjTranspose_same {A : Matrix n n R} {B : Matrix m n R} (hA : A.PosDef)
    (hB : Function.Injective B.vecMul) : (B * A * Bᴴ).PosDef :=
  by
  replace hB := star_injective.comp <| hB.comp star_injective
  simp_rw [Function.comp_def, star_vecMul, star_star] at hB
  simpa using hA.conjTranspose_mul_mul_same (B := Bᴴ) hB

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