English
Let s ⊆ E with UniqueDiffWithinAt x. Then the norm of the first iterated derivative of f within s at x equals the norm of the corresponding first derivative: ||iteratedFDerivWithin 𝕜 1 f s x|| = ||fderivWithin 𝕜 f s x||.
Русский
Пусть s ⊆ E имеет UniqueDiffWithinAt в точке x. Тогда норма первого повторного производного функции внутри s в точке x равна норме соответствующей производной: ||iteratedFDerivWithin 𝕜 1 f s x|| = ||fderivWithin 𝕜 f s x||.
LaTeX
$$$\| \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(1)} f\,s\,x \| = \| fderivWithin_{\mathbb{K}} f\,s\,x \|$$$
Lean4
@[simp]
theorem norm_iteratedFDerivWithin_one (f : E → F) (h : UniqueDiffWithinAt 𝕜 s x) :
‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖ :=
by
simp only [← norm_fderivWithin_iteratedFDerivWithin, iteratedFDerivWithin_zero_eq_comp,
LinearIsometryEquiv.comp_fderivWithin _ h]
apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.norm_toContinuousLinearMap_comp
