hasFDerivAt_toLp — Mathlib

English

The derivative of the map toLp at f is the inverse equivalence’s differential, i.e. the derivative equals the symmetrized continuous linear map from the inverse of the equivalence.

Русский

Производная отображения к дляLp в точке f равна дифференциалу обратной эквивалентности, то есть производная равна линейному отображению, полученному из обратной эквивалентности.

LaTeX

$$$ \text{HasFDerivAt}\big( \text{toLp} , (\mathrm{continuousLinearEquiv}(p, 𝕜, \_)).\mathrm{symm}.\mathrm{toContinuousLinearMap}, f \big) $$$

Lean4

theorem hasFDerivAt_toLp (f : ∀ i, E i) :
    HasFDerivAt (toLp p) (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
  (hasStrictFDerivAt_toLp p f).hasFDerivAt

Похожие утверждения