Theorems · Theorem · complex analysis

Complex.hasSum_taylorSeries_on_eball

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄
  ⦃r : ENNReal⦄,
  DifferentiableOn ℂ f (Metric.eball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.eball c r → HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

A function that is complex differentiable on the open ball of radius r ≤ ∞ around c is given by evaluating its Taylor series at c on this open ball.

Defined in

Mathlib.Analysis.Complex.TaylorSeries

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace