English
The derivative of the equivalence WithLp.equiv between the appropriate spaces is the corresponding continuous linear map, i.e. the derivative at f is given by the continuous linear map associated to the equivalence.
Русский
Производная эквивалентности WithLp.equiv между соответствующими пространствами равна соответствующему непрерывному линейному отображению, то есть производная в f задаётся линейным отображением, ассоциированным с эквивалентностью.
LaTeX
$$$ \text{HasFDerivAt}\big( \mathrm{WithLp.equiv} , (\mathrm{continuousLinearEquiv}(p, 𝕜, \_)).\mathrm{toContinuousLinearMap}, f \big) $$$
Lean4
@[deprecated hasFDerivAt_ofLp (since := "2025-05-07")]
theorem hasFDerivAt_equiv (f : PiLp p E) :
HasFDerivAt (WithLp.equiv _ _) (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
hasFDerivAt_ofLp _ f
