English
If f is n-times continuously differentiable at x within a set s (with respect to 𝕜'), then the n-th iterated Fréchet derivative within s, after restricting scalars to 𝕜, coincides with the n-th iterated Fréchet derivative within s with respect to 𝕜, near x inside s.
Русский
Если f в точке x внутри области s является n-раз непрерывно дифференцируемой относительно 𝕜', то n-й итеративный Фреше-дератив внутри s, ограниченный по скалярам к 𝕜, совпадает с n-м итеративным Фреше-деративом внутри s относительно 𝕜 в окрестности x в s.
LaTeX
$$$ (\mathrm{restrictScalars}\, \mathbb{K}) \circ (\mathrm{iteratedFDerivWithin}_{\mathbb{K}'}^{n} f\, s) =^\text{nhdsWithin}_{x} (\mathrm{iteratedFDerivWithin}_{\mathbb{K}}^{n} f\, s) \,,$$$
Lean4
/-- If `f` is `n` times continuously differentiable at `x` within `s`, then the `n`th iterated Fréchet
derivative within `s` with respect to `𝕜` equals scalar restriction of the `n`th iterated Fréchet
derivative within `s` with respect to `𝕜'`.
-/
theorem restrictScalars_iteratedFDerivWithin_eventuallyEq (h : ContDiffWithinAt 𝕜' n f s x) (hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s) : (restrictScalars 𝕜) ∘ (iteratedFDerivWithin 𝕜' n f s) =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s := by
induction n with
| zero =>
filter_upwards with a
ext m
simp
| succ n hn =>
have t₀ := h.of_le (Nat.cast_le.mpr (n.le_add_right 1))
have t₁ : ∀ᶠ (y : E) in 𝓝[s] x, ContDiffWithinAt 𝕜' (↑(n + 1)) f s y :=
by
nth_rw 2 [← s.insert_eq_of_mem hx]
apply h.eventually (by simp)
filter_upwards [eventually_eventually_nhdsWithin.2 (hn t₀), t₁, eventually_mem_nhdsWithin (a := x) (s := s)] with a
h₁a h₃a h₄a
rw [← Filter.EventuallyEq] at h₁a
ext m
simp only [Function.comp_apply, coe_restrictScalars, iteratedFDerivWithin_succ_apply_left]
rw [← (h₁a.fderivWithin' (by tauto)).eq_of_nhdsWithin h₄a, fderivWithin_restrictScalars_comp]
· simp
· apply h₃a.differentiableWithinAt_iteratedFDerivWithin
· rw [Nat.cast_lt]
simp
· have : UniqueDiffOn 𝕜' s := hs.mono_field
simpa [s.insert_eq_of_mem h₄a]
apply hs a h₄a
