English
Uniform convergence on ct thickening implies convergence of cderiv composed with F to cderiv δ f.
Русский
Равномерная сходимость на ct-thickening имплицирует сходимость cderiv.
LaTeX
$$$TendstoUniformlyOn (cderiv δ) \\circ F (f) φ K$$
Lean4
/-- The logarithmic derivative of a sequence of functions converging locally uniformly to a
function is the logarithmic derivative of the limit function. -/
theorem logDeriv_tendsto {ι : Type*} {p : Filter ι} {f : ι → ℂ → ℂ} {g : ℂ → ℂ} {s : Set ℂ} (hs : IsOpen s) (x : s)
(hF : TendstoLocallyUniformlyOn f g p s) (hf : ∀ᶠ n : ι in p, DifferentiableOn ℂ (f n) s) (hg : g x ≠ 0) :
Tendsto (fun n : ι => logDeriv (f n) x) p (𝓝 ((logDeriv g) x)) :=
by
simp_rw [logDeriv]
apply Tendsto.div ((hF.deriv hf hs).tendsto_at x.2) (hF.tendsto_at x.2) hg
