Convergence of Taylor series of holomorphic functions

We show that the Taylor series around some point c : ℂ of a function f that is complex differentiable on the open ball of radius r around c converges to f on that open ball; see Complex.hasSum_taylorSeries_on_ball and Complex.taylorSeries_eq_on_ball for versions (in terms of HasSum and tsum, respectively) for functions to a complete normed space over ℂ, and Complex.taylorSeries_eq_on_ball' for a variant when f : ℂ → ℂ.

There are corresponding statements for Metric.eballs; see Complex.hasSum_taylorSeries_on_eball, Complex.taylorSeries_eq_on_eball and Complex.taylorSeries_eq_on_ball'.

We also show that the Taylor series around some point c : ℂ of a function f that is complex differentiable on all of ℂ converges to f on ℂ; see Complex.hasSum_taylorSeries_of_entire, Complex.taylorSeries_eq_of_entire and Complex.taylorSeries_eq_of_entire'.

theorem Complex.hasSum_taylorSeries_on_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄ (hf : DifferentiableOn ℂ f (Metric.ball c r)) ⦃z : ℂ⦄ (hz : 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.

theorem Complex.taylorSeries_eq_on_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ℝ⦄ (hf : DifferentiableOn ℂ f (Metric.ball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c r) : ∑' (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.

theorem Complex.taylorSeries_eq_on_ball' ⦃c : ℂ⦄ ⦃r : ℝ⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = 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.

theorem Complex.hasSum_taylorSeries_on_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : 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.

@[deprecated Complex.hasSum_taylorSeries_on_eball (since := "2026-01-24")]

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

Alias of Complex.hasSum_taylorSeries_on_eball.

---

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.

theorem Complex.taylorSeries_eq_on_eball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : ∑' (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.

@[deprecated Complex.taylorSeries_eq_on_eball (since := "2026-01-24")]

theorem Complex.taylorSeries_eq_on_emetric_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ (hf : DifferentiableOn ℂ f (Metric.eball c r)) ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z

Alias of Complex.taylorSeries_eq_on_eball.

---

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.

theorem Complex.taylorSeries_eq_on_eball' ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.eball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = 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.

@[deprecated Complex.taylorSeries_eq_on_eball' (since := "2026-01-24")]

theorem Complex.taylorSeries_eq_on_emetric_ball' ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.eball c r) {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.eball c r)) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Alias of Complex.taylorSeries_eq_on_eball'.

---

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.

theorem Complex.hasSum_taylorSeries_of_entire {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ (hf : Differentiable ℂ f) (c z : ℂ) : HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

A function that is complex differentiable on the complex plane is given by evaluating its Taylor series at any point c.

theorem Complex.taylorSeries_eq_of_entire {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄ (hf : Differentiable ℂ f) (c z : ℂ) : ∑' (n : ℕ), (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z

A function that is complex differentiable on the complex plane is given by evaluating its Taylor series at any point c.

theorem Complex.taylorSeries_eq_of_entire' (c z : ℂ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) : ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

A function that is complex differentiable on the complex plane is given by evaluating its Taylor series at any point c.