English
If a complex function f: ℂ → E is differentiable on a punctured domain near c and f(z)−f(c) is o(|z−c|), then the modified function that uses limUnder along 𝓝[≠] c is differentiable on the same domain.
Русский
Если f: ℂ → E дифференцируема на окружности вокруг c без самой точки c и f(z)−f(c)=o(|z−c|), то соответствующая функция с пределом продолжения на c тоже дифференцируема на том же множестве.
LaTeX
$$$\displaystyle \text{If } f: \mathbb{C} \to E \text{ is differentiable on } s\setminus\{c\} \text{ and } f(z)-f(c)=o(|z-c|),$ \\ "update f at c" \text{ is differentiable on } s.$$
Lean4
/-- **Removable singularity** theorem, weak version. If `f : ℂ → E` is differentiable in a punctured
neighborhood of a point and is continuous at this point, then it is analytic at this point. -/
theorem analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt {f : ℂ → E} {c : ℂ}
(hd : ∀ᶠ z in 𝓝[≠] c, DifferentiableAt ℂ f z) (hc : ContinuousAt f c) : AnalyticAt ℂ f c :=
by
rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 hd with ⟨R, hR0, hRs⟩
lift R to ℝ≥0 using hR0.le
replace hc : ContinuousOn f (closedBall c R) :=
by
refine fun z hz => ContinuousAt.continuousWithinAt ?_
rcases eq_or_ne z c with (rfl | hne)
exacts [hc, (hRs ⟨hz, hne⟩).continuousAt]
exact
(hasFPowerSeriesOnBall_of_differentiable_off_countable (countable_singleton c) hc
(fun z hz => hRs (diff_subset_diff_left ball_subset_closedBall hz)) hR0).analyticAt
