Theorems · Theorem · complex analysis

Complex.differentiableOn_update_limUnder_of_isLittleO

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ}
  {c : ℂ},
  s ∈ nhds c →
    DifferentiableOn ℂ f (s \ {c}) →
      ((fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) →
        DifferentiableOn ℂ (Function.update f c ((nhdsWithin c {c}ᶜ).limUnder 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.

Defined in

Mathlib.Analysis.Complex.RemovableSingularity

Cited by

4 results in Mathlib

Foundations

Depth 286 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace