English
The map that relates PiLp p E to its realization via the corresponding linear isomorphism is Frechet differentiable at every f, with derivative the continuous linear map given by the associated continuous linear equivalence.
Русский
Отображение, переводящее PiLp p E к его реализации через соответствующее линейное изоморфизм, дифференцируемо по Фреше в любой точке f; производная задаётся линейным отображением, соответствующим непрерывному линейному эквиваленту.
LaTeX
$$$ \text{HasFDerivAt}\big( \text{ofLp} , (\mathrm{continuousLinearEquiv}(p, 𝕜, \_)).\mathrm{toContinuousLinearMap}, f \big) $$$
Lean4
theorem hasFDerivAt_ofLp (f : PiLp p E) : HasFDerivAt ofLp (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
(hasStrictFDerivAt_ofLp p f).hasFDerivAt
