English
Let s be an open subset of the field 𝕜. Suppose f_n: 𝕜 → G and g: 𝕜 → G with f'_n: 𝕜 → G and g' : 𝕜 → G satisfy that f'_n tend locally uniformly to g' on s along l, and that for all x ∈ s, eventually in l the maps x ↦ f_n have derivative f'_n x at x, and that f_n x → g x for every x ∈ s. Then for every x ∈ s, g is differentiable at x with derivative g'(x).
Русский
Пусть s ⊂ 𝕜 открыто. Пусть f_n: 𝕜 → G, g: 𝕜 → G, а f'_n: 𝕜 → G и g' : 𝕜 → G. Предположим, что f'_n сходятся локально равномерно к g' на s по l, и что для всех x ∈ s существует N, что для всех n ≥ N у f_n существует производная f'_n x в точке x, и что f_n x → g x по l для всех x ∈ s. Тогда для каждого x ∈ s функция g дифференцируема в x, производная равна g'(x).
LaTeX
$$$IsOpen(s) \to TendstoLocallyUniformlyOn\ f'\ g'\ l\ s \\to (\forallᶠ n in l, \forall x \in s, HasDerivAt (f n) (f' n x) x) \\to (\forall x \in s, Tendsto (fun n => f n x) l (\mathcal{N} (g x))) \\to \forall x \in s, HasDerivAt g (g' x) x$$$
Lean4
theorem hasDerivAt_of_tendstoLocallyUniformlyOn [NeBot l] {s : Set 𝕜} (hs : IsOpen s)
(hf' : TendstoLocallyUniformlyOn f' g' l s) (hf : ∀ᶠ n in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x)
(hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasDerivAt g (g' x) x :=
by
have h1 : s ∈ 𝓝 x := hs.mem_nhds hx
have h2 : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2 :=
eventually_prod_iff.2 ⟨_, hf, fun x => x ∈ s, h1, fun {n} => id⟩
refine hasDerivAt_of_tendstoUniformlyOnFilter ?_ h2 (eventually_of_mem h1 hfg)
simpa [IsOpen.nhdsWithin_eq hs hx] using tendstoLocallyUniformlyOn_iff_filter.mp hf' x hx
