English
Removable singularity: if s is a punctured neighborhood of c, f is differentiable on s, and f(z)−f(c)=o((z−c)^{-1}), then the updated function is differentiable on {c} ∪ s.
Русский
Устранимая особенность: если s — punctured neighbourhood of c, f дифференцируема на s и f(z)−f(c)=o((z−c)^{-1}), то обновленная функция дифференцируема на {c} ∪ s.
LaTeX
$$$\text{DifferentiableOn}(\mathbb{C}, f, s) \land (f(z)-f(c)) =o_{\mathcal{N}[\neq] c} (z-c)^{-1} \Rightarrow \text{DifferentiableOn}(\mathbb{C}, \text{update}(f,c,\limUnder(\mathcal{N}[\neq] c) f), \text{insert}(c,s))$$$
Lean4
/-- **Removable singularity** theorem: if `s` is a punctured neighborhood of `c : ℂ`, a function
`f : ℂ → E` is complex differentiable on `s`, 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 `{c} ∪ s`. -/
theorem differentiableOn_update_limUnder_insert_of_isLittleO {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝[≠] c)
(hd : DifferentiableOn ℂ f s) (ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹) :
DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) (insert c s) :=
differentiableOn_update_limUnder_of_isLittleO (insert_mem_nhds_iff.2 hc) (hd.mono fun _ hz => hz.1.resolve_left hz.2)
ho
