English
If a function is differentiable on a domain and is bounded on the punctured part near c, then updating by limUnder preserves differentiability on the whole set.
Русский
Если функция дифференцируема на области и ограничена на дырчатой части поблизости к c, обновление limUnder сохраняет дифференцируемость на всей области.
LaTeX
$$$\text{If } f: \mathbb{C} \to E,\ hc,\ hd,\ hb,\ \text{ then } differentiableOn\ (update f c (limUnder (nhdsWithin c) f)) s.$$$
Lean4
/-- **Removable singularity** theorem: if `s` is a neighborhood of `c : ℂ`, a function `f : ℂ → E`
is complex differentiable and is bounded on `s \ {c}`, then `f` redefined to be equal to
`limUnder (𝓝[≠] c) f` at `c` is complex differentiable on `s`. -/
theorem differentiableOn_update_limUnder_of_bddAbove {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ 𝓝 c)
(hd : DifferentiableOn ℂ f (s \ { c })) (hb : BddAbove (norm ∘ f '' (s \ { c }))) :
DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) s :=
differentiableOn_update_limUnder_of_isLittleO hc hd <|
IsBoundedUnder.isLittleO_sub_self_inv <|
let ⟨C, hC⟩ := hb
⟨C + ‖f c‖,
eventually_map.2 <|
mem_nhdsWithin_iff_exists_mem_nhds_inter.2
⟨s, hc, fun _ hz => norm_sub_le_of_le (hC <| mem_image_of_mem _ hz) le_rfl⟩⟩
