Theorems · Theorem · complex analysis

Complex.hasSum_taylorSeries_on_ball

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄,
  DifferentiableOn ℂ f (Metric.ball c r) →
    ∀ ⦃z : ℂ⦄, z ∈ Metric.ball 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 285 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace