mathlibdocumentation

analysis.complex.removable_singularity

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

theorem complex.analytic_at_of_differentiable_on_punctured_nhds_of_continuous_at {E : Type u} [normed_group E] [ E] {f : → E} {c : } (hd : ∀ᶠ (z : ) in {c}, ) (hc : c) :
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_compl_singleton_and_continuous_at_iff {E : Type u} [normed_group E] [ E] {f : → E} {s : set } {c : } (hs : s nhds c) :
(s \ {c})
theorem complex.differentiable_on_dslope {E : Type u} [normed_group E] [ E] {f : → E} {s : set } {c : } (hc : s nhds c) :
(dslope f c) s
theorem complex.differentiable_on_update_lim_of_is_o {E : Type u} [normed_group E] [ E] {f : → E} {s : set } {c : } (hc : s nhds c) (hd : (s \ {c})) (ho : asymptotics.is_o (λ (z : ), f z - f c) (λ (z : ), (z - c)⁻¹) {c})) :
c (lim {c}) f)) s

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_group E] [ E] {f : → E} {s : set } {c : } (hc : s {c}) (hd : s) (ho : asymptotics.is_o (λ (z : ), f z - f c) (λ (z : ), (z - c)⁻¹) {c})) :
c (lim {c}) f)) s)

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.

theorem complex.differentiable_on_update_lim_of_bdd_above {E : Type u} [normed_group E] [ E] {f : → E} {s : set } {c : } (hc : s nhds c) (hd : (s \ {c})) (hb : bdd_above '' (s \ {c}))) :
c (lim {c}) f)) 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.

theorem complex.tendsto_lim_of_differentiable_on_punctured_nhds_of_is_o {E : Type u} [normed_group E] [ E] {f : → E} {c : } (hd : ∀ᶠ (z : ) in {c}, ) (ho : asymptotics.is_o (λ (z : ), f z - f c) (λ (z : ), (z - c)⁻¹) {c})) :
{c}) (nhds (lim {c}) f))

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_lim_of_differentiable_on_punctured_nhds_of_bounded_under {E : Type u} [normed_group E] [ E] {f : → E} {c : } (hd : ∀ᶠ (z : ) in {c}, ) (hb : (λ (z : ), f z - f c)) :
{c}) (nhds (lim {c}) f))

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.