English
If f is n-times continuously differentiable at x within s (ContDiffWithinAt 𝕜' n f s x), and s has a unique differentiability structure, then restricting scalars to 𝕜 yields the Fréchet derivative within s with respect to 𝕜 at x, in the nhdsWithin s of x.
Русский
Если f дифференцируема в точке x внутри s в смысле ContDiffWithinAt 𝕜' n f s x и s имеет уникальную дифференцируемость, то ограничение скалярами к 𝕜 даёт производную Фреше внутри s в точке x в окрестности nhdsWithin s.
LaTeX
$$$ ContDiffWithinAt\ 𝕜'\ n f s x \Rightarrow (\restrictScalars\ 𝕜) \circ (\ iteratedFDerivWithin\ 𝕜'\ n f\ s) =^{{\ NHDSWithin x}} (\ iteratedFDerivWithin\ 𝕜\ n f\ s)$$$
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_eventuallyEq (h : ContDiffAt 𝕜' n f x) :
(restrictScalars 𝕜) ∘ (iteratedFDeriv 𝕜' n f) =ᶠ[𝓝 x] iteratedFDeriv 𝕜 n f :=
by
have h' : ContDiffWithinAt 𝕜' n f Set.univ x := h
convert (h'.restrictScalars_iteratedFDerivWithin_eventuallyEq _ trivial) <;>
simp [iteratedFDerivWithin_univ.symm, uniqueDiffOn_univ]
