English
The log-derivative of a locally uniformly convergent sequence converges to the log-derivative of the limit function, provided differentiability holds for the sequence and nonvanishing of the limit.
Русский
Логарифмическая производная последовательности, сходящейся локально по униформности, сходится к логарифмической производной предельной функции при условии дифференцируемости последовательности и ненулевости предела.
LaTeX
$$$Tendsto (\\lambda n, \\logDeriv (f n) x) p (\\mathcal{N} (\\logDeriv g x))$ under hypotheses$$
Lean4
/-- The **Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is continuous on a
closed disc of radius `R` and center `c`, and is complex differentiable at all but countably many
points of its interior, then the circle average `circleAverage f c R` equals `f c`.
-/
theorem circleAverage_of_differentiable_on_off_countable (hs : s.Countable) (h₁f : ContinuousOn f (closedBall c |R|))
(h₂f : ∀ z ∈ ball c |R| \ s, DifferentiableAt ℂ f z) : circleAverage f c R = f c :=
by
rcases lt_trichotomy 0 R with h | rfl | h
· rw [← abs_of_pos h]
exact circleAverage_of_differentiable_on_off_countable_posRadius (abs_pos_of_pos h) hs h₁f h₂f
· simp
· rw [← circleAverage_neg_radius, ← abs_of_neg h]
exact circleAverage_of_differentiable_on_off_countable_posRadius (abs_pos_of_neg h) hs h₁f h₂f
