English
If s is a neighborhood of c and f is differentiable on s except possibly at c with a little-o error around c, then updating f at c by limUnder of the punctured neighborhood yields differentiability on s.
Русский
Если s — окрестность c и f дифференцируема на s за исключением c с ошибкой, переход к limUnder по punctured окрестности сохраняет дифференцируемость на s после обновления в c.
LaTeX
$$$\text{Assume } s\ni c,\D f \text{ дифференцируемо на } s\setminus\{c\} \text{ и } f(z)-f(c)=o(\diam) \Rightarrow \text{ DifferentiableOn } (update f c (\limUnder (\mathcal{N}\setminus c) f)) s.$$$
Lean4
/-- **Removable singularity** theorem: if `s` is a neighborhood of `c : ℂ`, a function `f : ℂ → E`
is complex differentiable on `s \ {c}`, and $f(z) - f(c)=o((z-c)^{-1})$, then `f` redefined to be
equal to `limUnder (𝓝[≠] c) f` at `c` is complex differentiable on `s`. -/
theorem differentiableOn_update_limUnder_of_isLittleO {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝 c)
(hd : DifferentiableOn ℂ f (s \ { c })) (ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹) :
DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s :=
by
set F : ℂ → E := fun z => (z - c) • f z
suffices DifferentiableOn ℂ F (s \ { c }) ∧ ContinuousAt F c
by
rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc, dslope_sub_smul] at this
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) := continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
rwa [hc.limUnder_eq]
refine ⟨(differentiableOn_id.sub_const _).smul hd, ?_⟩
rw [← continuousWithinAt_compl_self]
have H := ho.tendsto_inv_smul_nhds_zero
have H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c)) :=
(continuousWithinAt_id.tendsto.sub tendsto_const_nhds).smul tendsto_const_nhds
simpa [← smul_add, ContinuousWithinAt] using H.add H'
