English
Let s be open and l a nontrivial index filter. Suppose TendstoLocallyUniformlyOn of (deriv ∘ f) to g' on s along l, and that eventually in l each f_n is differentiable on s. If f_n x → g x for all x ∈ s, then g is differentiable on s with derivative g'(x) for every x ∈ s.
Русский
Пусть s открыто, l — не тривиальный фильтр индексов. Пусть производная от f_n сходится локально по локальной однородной схеме к g' на s по l, и что в конечном счёте для всех n функции f_n дифференцируемы на s. Если для всех x ∈ s выполняется f_n x → g x по l, то g дифференцируема на s и имеет производную g'(x) в каждой точке x ∈ s.
LaTeX
$$$IsOpen(s) \to TendstoLocallyUniformlyOn (deriv \circ f) g' l s \to (\forallᶠ n in l, DifferentiableOn 𝕜 (f n) s) \\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
/-- A slight variant of `hasDerivAt_of_tendstoLocallyUniformlyOn` with the assumption stated in
terms of `DifferentiableOn` rather than `HasDerivAt`. This makes a few proofs nicer in complex
analysis where holomorphicity is assumed but the derivative is not known a priori. -/
theorem hasDerivAt_of_tendsto_locally_uniformly_on' [NeBot l] {s : Set 𝕜} (hs : IsOpen s)
(hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s) (hf : ∀ᶠ n in l, DifferentiableOn 𝕜 (f n) s)
(hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) : HasDerivAt g (g' x) x :=
by
refine hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx
filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt
