English
If derivatives converge uniformly on a neighborhood and the derivatives are differentiable, then the limit derivative exists uniformly as a function of x in the neighborhood.
Русский
Если производные сходятся равномерно на окрестности и сами дифференцируемы, то существует равномерно существующая пределная производная.
LaTeX
$$$\\forall x,\\ 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. -/
theorem hasFDerivAt_of_tendstoUniformly [NeBot l] (hf' : TendstoUniformly f' g' l)
(hf : ∀ n : ι, ∀ x : E, HasFDerivAt (f n) (f' n x) x) (hfg : ∀ x : E, Tendsto (fun n => f n x) l (𝓝 (g x)))
(x : E) : HasFDerivAt g (g' x) x :=
by
have hf : ∀ n : ι, ∀ x : E, x ∈ Set.univ → HasFDerivAt (f n) (f' n x) x := by simp [hf]
have hfg : ∀ x : E, x ∈ Set.univ → Tendsto (fun n => f n x) l (𝓝 (g x)) := by simp [hfg]
have hf' : TendstoUniformlyOn f' g' l Set.univ := by rwa [tendstoUniformlyOn_univ]
exact hasFDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)
