English
If f'_n tends uniformly to g' on l and each HasDerivAt (f n) (f' n x) x holds for all x, with the same hfg condition, then g has derivative g' at x for x ∈ s.
Русский
Если производные f'_n сходятся равномерно к g' по l на s и для каждого n выполняются HasDerivAt (f_n) (f'_n x) x при всех x, вместе с условием сходимости f_n x → g x, то у g в точке x есть производная g'(x).
LaTeX
$$$IsOpen(s) \to TendstoUniformlyOn f' g' l s \to (\forallᶠ n in l, \forall x ∈ s, HasDerivAt (f n) (f' n x) x) \\to (\forall x ∈ s, Tendsto (fun n => f n x) l (\mathcal{N} (g x))) \to \forall x ∈ s, HasDerivAt g (g' x) x$$$
Lean4
theorem hasDerivAt_of_tendstoUniformly [NeBot l] (hf' : TendstoUniformly f' g' l)
(hf : ∀ᶠ n in l, ∀ x : 𝕜, HasDerivAt (f n) (f' n x) x) (hfg : ∀ x : 𝕜, Tendsto (fun n => f n x) l (𝓝 (g x)))
(x : 𝕜) : HasDerivAt g (g' x) x :=
by
have hf : ∀ᶠ n in l, ∀ x : 𝕜, x ∈ Set.univ → HasDerivAt (f n) (f' n x) x := by
filter_upwards [hf] with n h x _ using h x
have hfg : ∀ x : 𝕜, 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 hasDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)
