English
If a sequence of derivatives converges uniformly on a neighborhood, and the functions converge pointwise, then the limit function is differentiable with the limit derivative.
Русский
Если последовательность производных сходится равномерно на окрестности, а функции сходятся по точкам, то предел дифференцируем, и его производная равна пределу производных.
LaTeX
$$$\\text{If } hf' : TendstoUniformlyOnFilter f' g' l (\\mathcal{N} x) \\, \\text{and } hf, hfg, \\text{ then } HasFDerivAt g (g' x) x$$$
Lean4
/-- `(d/dx) lim_{n → ∞} f n x = lim_{n → ∞} f' n x` when the `f' n` converge
_uniformly_ to their limit on an open set containing `x`. -/
theorem hasFDerivAt_of_tendstoUniformlyOn [NeBot l] {s : Set E} (hs : IsOpen s) (hf' : TendstoUniformlyOn f' g' l s)
(hf : ∀ n : ι, ∀ x : E, x ∈ s → HasFDerivAt (f n) (f' n x) x)
(hfg : ∀ x : E, x ∈ s → Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasFDerivAt g (g' x) x :=
hasFDerivAt_of_tendstoLocallyUniformlyOn hs hf'.tendstoLocallyUniformlyOn hf hfg hx
