Documentation

Mathlib.Analysis.Complex.RemovableSingularity

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.

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.

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.

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.

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.

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.

The Cauchy formula for the derivative of a holomorphic function.