adjoint_conj — Mathlib

English

For a positive linear map T and a linear map S, the operator S.adjoint ∘ T ∘ S is positive.

Русский

Для положительного линейного отображения T и линейного отображения S, оператор S.adjoint ∘ T ∘ S положителен.

LaTeX

$$$\text{IsPositive}(S^\ast \circ T \circ S)$$$

Lean4

@[aesop safe apply]
theorem adjoint_conj {T : E →L[𝕜] E} (hT : T.IsPositive) (S : F →L[𝕜] E) : (S† ∘L T ∘L S).IsPositive :=
  by
  convert hT.conj_adjoint (S†)
  rw [adjoint_adjoint]

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