English
If f is n-times continuously differentiable at x, then restricting scalars to 𝕜 yields equality between the n-th iterated Fréchet derivative with respect to 𝕜 and the restricted 𝕜'-derivative at x.
Русский
Если f является n-раз непрерывно дифференцируемой в точке x, то ограничение по скалярам к 𝕜 даёт равенство между n-й итеративной Фреше-деративой относительно 𝕜 и ограниченной 𝕜'-деривацией в точке x.
LaTeX
$$$ (\restrictScalars\ 𝕜) \circ (\ iteratedFDeriv\ 𝕜'\ n f) =^{{\ NHDS x}} (\ iteratedFDeriv\ 𝕜\ n f) \;,$$$
Lean4
/-- If `f` is `n` times continuously differentiable at `x`, then the `n`th iterated Fréchet derivative
with respect to `𝕜` equals scalar restriction of the `n`th iterated Fréchet derivative with respect
to `𝕜'`.
-/
theorem restrictScalars_iteratedFDeriv (h : ContDiffAt 𝕜' n f x) :
((restrictScalars 𝕜) ∘ iteratedFDeriv 𝕜' n f) x = iteratedFDeriv 𝕜 n f x :=
h.restrictScalars_iteratedFDeriv_eventuallyEq.eq_of_nhds
