𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ reApplyInnerSelf (comp S (comp T (↑adjoint S))) x
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
⊢ IsPositive (comp S (comp T (↑adjoint S)))
refine' ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => _⟩
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ ↑re (inner (↑(comp T (↑adjoint S)) x) (↑(↑adjoint S) x))
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ reApplyInnerSelf (comp S (comp T (↑adjoint S))) x
rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ ↑re (inner (↑(comp T (↑adjoint S)) x) (↑(↑adjoint S) x))
exact hT.inner_nonneg_left _