English
Let T be a self-adjoint bounded operator on an inner product space E and let S be a bounded operator from F to E. Then the compressed operator S^* T S is self-adjoint on F. In other words, conjugating a self-adjoint operator by S preserves self-adjointness.
Русский
Пусть T — самосопряжённый ограниченный оператор на внутренне произведённом пространстве E, и пусть S: F → E — ограниченный оператор. Тогда сжатие T до пространства F через S, то есть S^* T S, является самосопряжённым на F.
LaTeX
$$$\\text{If } T \\text{ is self-adjoint, then } S^{*} T S \\text{ is self-adjoint},$$$
Lean4
/-- Conjugating preserves self-adjointness. -/
theorem adjoint_conj {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : F →L[𝕜] E) : IsSelfAdjoint (S.adjoint ∘L T ∘L S) :=
by
rw [isSelfAdjoint_iff'] at hT ⊢
simp only [hT, adjoint_comp, adjoint_adjoint]
exact ContinuousLinearMap.comp_assoc _ _ _
