Documentation

Mathlib.Analysis.Complex.TaylorSeries

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 EMEtric.balls; see Complex.hasSum_taylorSeries_on_emetric_ball, Complex.taylorSeries_eq_on_emetric_ball 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_emetric_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : } {r : ENNReal} (hf : DifferentiableOn f (EMetric.ball c r)) {z : } (hz : z EMetric.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_emetric_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : E} {c : } {r : ENNReal} (hf : DifferentiableOn f (EMetric.ball c r)) {z : } (hz : z EMetric.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_emetric_ball' {c : } {r : ENNReal} {z : } (hz : z EMetric.ball c r) {f : } (hf : DifferentiableOn f (EMetric.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_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.