Theorems · Theorem · complex analysis

Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : NNReal} {c : ℂ}
  {f : ℂ → E} {s : Set ℂ},
  s.Countable →
    ContinuousOn f (Metric.closedBall c ↑R) →
      (∀ z ∈ Metric.ball c ↑R \ s, DifferentiableAt ℂ f z) →
        0 < R → HasFPowerSeriesOnBall f (cauchyPowerSeries f c ↑R) c ↑R

If f : ℂ → E is continuous on a closed ball of positive radius and is differentiable at all but countably many points of the corresponding open ball, then it is analytic on the open ball with coefficients of the power series given by Cauchy integral formulas.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace