English
The action of the adjoint auxiliary operator on a vector equals a composition with the dual map, i.e., adjointAux A applied to y equals the dual map of E composed with the sesquilinear form applied to y and A.
Русский
Действие вспомогательного сопряжённого оператора на вектор равно композиции с двойственным отображением через форму, т.е. adjointAux A применён к y равен симметричному двойственному отображению, применённому к y и A.
LaTeX
$$$$ \\big( \\mathrm{adjointAux} \\; A \\big) x = ((\\mathrm{toDual}\\; 𝕜\, E)^{ -1}) (\\mathrm{toSesqForm} A\, x). $$$$
Lean4
/-- The adjoint, as a continuous conjugate-linear map. This is only meant as an auxiliary
definition for the main definition `adjoint`, where this is bundled as a conjugate-linear isometric
equivalence. -/
noncomputable def adjointAux : (E →L[𝕜] F) →L⋆[𝕜] F →L[𝕜] E :=
(ContinuousLinearMap.compSL _ _ _ _ _ ((toDual 𝕜 E).symm : StrongDual 𝕜 E →L⋆[𝕜] E)).comp
(toSesqForm : (E →L[𝕜] F) →L[𝕜] F →L⋆[𝕜] StrongDual 𝕜 E)
