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} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} (hd : ∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) (hc : ContinuousAt f c) : AnalyticAt ℂ f 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.differentiableOn_compl_singleton_and_continuousAt_iff {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hs : s ∈ nhds c) : DifferentiableOn ℂ f (s \ {c}) ∧ ContinuousAt f c ↔ DifferentiableOn ℂ f s

theorem Complex.differentiableOn_dslope {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ nhds c) : DifferentiableOn ℂ (dslope f c) s ↔ DifferentiableOn ℂ f s

theorem Complex.differentiableOn_update_limUnder_of_isLittleO {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {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)⁻¹) : DifferentiableOn ℂ (Function.update f c (limUnder (nhdsWithin c {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 limUnder (𝓝[≠] c) f at c is complex differentiable on s.

theorem Complex.differentiableOn_update_limUnder_insert_of_isLittleO {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ nhdsWithin c {c}ᶜ) (hd : DifferentiableOn ℂ f s) (ho : (fun (z : ℂ) => f z - f c) =o[nhdsWithin c {c}ᶜ] fun (z : ℂ) => (z - c)⁻¹) : DifferentiableOn ℂ (Function.update f c (limUnder (nhdsWithin c {c}ᶜ) f)) (insert c 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.

theorem Complex.differentiableOn_update_limUnder_of_bddAbove {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ nhds c) (hd : DifferentiableOn ℂ f (s \ {c})) (hb : BddAbove (norm ∘ f '' (s \ {c}))) : DifferentiableOn ℂ (Function.update f c (limUnder (nhdsWithin c {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 limUnder (𝓝[≠] c) f at c is complex differentiable on s.

theorem Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} (hd : ∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) (ho : (fun (z : ℂ) => f z - f c) =o[nhdsWithin c {c}ᶜ] fun (z : ℂ) => (z - c)⁻¹) : Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds (limUnder (nhdsWithin c {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_limUnder_of_differentiable_on_punctured_nhds_of_bounded_under {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {c : ℂ} (hd : ∀ᶠ (z : ℂ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℂ f z) (hb : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin c {c}ᶜ) fun (z : ℂ) => ‖f z - f c‖) : Filter.Tendsto f (nhdsWithin c {c}ᶜ) (nhds (limUnder (nhdsWithin c {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.

theorem Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} (hU : IsOpen U) {c w₀ : ℂ} {R : ℝ} {f : ℂ → E} (hc : Metric.closedBall c R ⊆ U) (hf : DifferentiableOn ℂ f U) (hw₀ : w₀ ∈ Metric.ball c R) : ((2 * ↑Real.pi * I)⁻¹ • ∮ (z : ℂ) in C(c, R), ((z - w₀) ^ 2)⁻¹ • f z) = deriv f w₀

The Cauchy formula for the derivative of a holomorphic function.