mathlib3 documentation

analysis.complex.removable_singularity

Removable singularity theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 function.update f c (lim (𝓝[≠] c) f) is complex differentiable in a neighborhood of c.

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.differentiable_on_update_lim_of_is_o {E : Type u} [normed_add_comm_group E] [normed_space E] [complete_space E] {f : E} {s : set } {c : } (hc : s nhds c) (hd : differentiable_on f (s \ {c})) (ho : (λ (z : ), f z - f c) =o[nhds_within c {c}] λ (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 lim (𝓝[≠] c) f at c is complex differentiable on s.

theorem complex.differentiable_on_update_lim_insert_of_is_o {E : Type u} [normed_add_comm_group E] [normed_space E] [complete_space E] {f : E} {s : set } {c : } (hc : s nhds_within c {c}) (hd : differentiable_on f s) (ho : (λ (z : ), f z - f c) =o[nhds_within c {c}] λ (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 lim (𝓝[≠] c) f at c is complex differentiable on {c} ∪ s.

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 lim (𝓝[≠] c) f at c is complex differentiable on s.

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.

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_circle_integral_sub_sq_inv_smul_of_differentiable {E : Type u} [normed_add_comm_group E] [normed_space E] [complete_space E] {U : set } (hU : is_open U) {c w₀ : } {R : } {f : E} (hc : metric.closed_ball c R U) (hf : differentiable_on f U) (hw₀ : w₀ metric.ball c R) :
(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.