English
Under appropriate neighborhood convergence assumptions, iterated derivatives converge in the sense of eventually equalities to the corresponding derivatives of the limit function.
Русский
При подходящих условиях сходимости по окрестностям, повторные производные сходятся в смысле предельного равенства к соответствующим производным предельной функции.
LaTeX
$$$f_{n} \to f \Rightarrow \forall n, \operatorname{iteratedFDerivWithin} f_{n} \to \operatorname{iteratedFDerivWithin} f$$$
Lean4
theorem iteratedFDerivWithin' (h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t := by
induction n with
| zero => exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy
| succ n ihn =>
have : fderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht
refine this.mono fun y hy => ?_
simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]
