# Removable singularity theorem #

In this file we prove Riemann's removable singularity theorem: if f : โ โ E is complex differentiable in a punctured neighborhood of a point c and is bounded in a punctured neighborhood of c (or, more generally, $f(z) - f(c)=o((z-c)^{-1})$), then it has a limit at c and the function update f c (limUnder (๐[โ ] c) f) is complex differentiable in a neighborhood of c.

theorem Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt {E : Type u} [] [] {f : โ โ E} {c : โ} (hd : โแถ  (z : โ) in nhdsWithin c {c}แถ, ) (hc : ) :

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 Complex.differentiableOn_dslope {E : Type u} [] [] {f : โ โ E} {s : } {c : โ} (hc : s โ nhds c) :
theorem Complex.differentiableOn_update_limUnder_of_isLittleO {E : Type u} [] [] {f : โ โ E} {s : } {c : โ} (hc : s โ nhds c) (hd : DifferentiableOn โ f (s \ {c})) (ho : (fun (z : โ) => f z - f c) =o[nhdsWithin c {c}แถ] fun (z : โ) => (z - c)โปยน) :

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 Complex.differentiableOn_update_limUnder_insert_of_isLittleO {E : Type u} [] [] {f : โ โ E} {s : } {c : โ} (hc : s โ nhdsWithin c {c}แถ) (hd : ) (ho : (fun (z : โ) => f z - f c) =o[nhdsWithin c {c}แถ] fun (z : โ) => (z - c)โปยน) :

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 Complex.differentiableOn_update_limUnder_of_bddAbove {E : Type u} [] [] {f : โ โ E} {s : } {c : โ} (hc : s โ nhds c) (hd : DifferentiableOn โ f (s \ {c})) (hb : BddAbove (norm โ f '' (s \ {c}))) :

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 Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO {E : Type u} [] [] {f : โ โ E} {c : โ} (hd : โแถ  (z : โ) in nhdsWithin c {c}แถ, ) (ho : (fun (z : โ) => f z - f c) =o[nhdsWithin c {c}แถ] fun (z : โ) => (z - c)โปยน) :

Removable singularity theorem: if a function f : โ โ E is complex differentiable on a punctured neighborhood of c and $f(z) - f(c)=o((z-c)^{-1})$, then f has a limit at c.

theorem Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under {E : Type u} [] [] {f : โ โ E} {c : โ} (hd : โแถ  (z : โ) in nhdsWithin c {c}แถ, ) (hb : Filter.IsBoundedUnder (fun (x x_1 : โ) => x โค x_1) (nhdsWithin c {c}แถ) fun (z : โ) => โf z - f cโ) :

Removable singularity theorem: if a function f : โ โ E is complex differentiable and bounded on a punctured neighborhood of c, then f has a limit at c.

theorem Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable {E : Type u} [] [] {U : } (hU : ) {c : โ} {wโ : โ} {R : โ} {f : โ โ E} (hc : โ U) (hf : ) (hwโ : wโ โ ) :
((2 * โReal.pi * Complex.I)โปยน โข โฎ (z : โ) in C(c, R), ((z - wโ) ^ 2)โปยน โข f z) = deriv f wโ

The Cauchy formula for the derivative of a holomorphic function.