isPositive_self_comp_adjoint

Mathlib.Analysis.InnerProductSpace.Positive

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isPositive_self_comp_adjoint

English

If T is positive, then for any S: F → E, the operator S† ∘ T ∘ S is positive.

Русский

Если T положителен, то для любого S: F → E оператор S† ∘ T ∘ S положителен.

LaTeX

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

Lean4

theorem isPositive_self_comp_adjoint (S : E →L[𝕜] F) : (S ∘L S†).IsPositive := by
  simpa using isPositive_one.conj_adjoint S

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru