hasStrictFDerivAt_ofLp — Mathlib

English

A PiLp-valued map is differentiable at a point if and only if all its coordinate maps are differentiable at that point.

Русский

Функция, принимающая значения в PiLp, дифференцируема в точке тогда и только тогда, когда все её координатные отображения дифференцируемы в этой точке.

LaTeX

$$$$ \\text{DifferentiableAt } f y \\iff \\forall i, \\text{DifferentiableAt } (fun x => f x i) y. $$$$

Lean4

theorem hasStrictFDerivAt_ofLp (f : PiLp p E) :
    HasStrictFDerivAt ofLp (continuousLinearEquiv p 𝕜 _).toContinuousLinearMap f :=
  .of_isLittleO <| (Asymptotics.isLittleO_zero _ _).congr_left fun _ => (sub_self _).symm

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