conjTranspose_mul_mul_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{mulVec}) \\to \\operatorname{PosDef}(B^{\\mathrm{H}} A B). $$$$

Lean4

theorem conjTranspose_mul_mul_same {A : Matrix n n R} {B : Matrix n m R} (hA : A.PosDef)
    (hB : Function.Injective B.mulVec) : (Bᴴ * A * B).PosDef :=
  by
  refine ⟨Matrix.isHermitian_conjTranspose_mul_mul _ hA.1, fun x hx => ?_⟩
  have : B *ᵥ x ≠ 0 := fun h => hx <| hB.eq_iff' (mulVec_zero _) |>.1 h
  simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.2 _ this

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