hasStrictFDerivAt_toLp — Mathlib

English

The symmetric counterpart of the previous derivative statement; the symmetrized derivative exists for the inverse equivalence.

Русский

Гармонизированная версия предыдущего утверждения о производной; симметричная производная существует для обработки обратного эквивалента.

LaTeX

$$$$ HasStrictFDerivAt\\bigl( (WithLp.equiv p ((i) → E i))^{ -1} \\bigr) \\bigl( (PiLp.continuousLinearEquiv p 𝕜 E)^{ -1} \\bigr). $$$$

Lean4

theorem hasStrictFDerivAt_toLp (f : ∀ i, E i) :
    HasStrictFDerivAt (toLp p) (continuousLinearEquiv p 𝕜 _).symm.toContinuousLinearMap f :=
  .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm

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