Taylor's Theorem for Complex Analytic Functions

Formalization of Theorem 1 (Taylor's Theorem) from Lecture 10 of MIT 18.112 (Functions of a Complex Variable, Fall 2008).

Main results

• complexTaylorPoly — the complex Taylor polynomial of degree n-1.
• taylor_complex — Part 1: If f is analytic in a region Ω containing a, then f(z) = f(a) + f'(a)/1! (z-a) + ⋯ + f^(n-1)(a)/(n-1)! (z-a)^(n-1) + fₙ(z)(z-a)^n where fₙ is analytic (differentiable) in Ω.
• taylor_integral_representation — Part 2: The integral representation of the remainder, fₙ(z) = (2πi)⁻¹ ∮_C f(ζ) dζ / ((ζ-a)^n(ζ-z)), proved by induction on n using Cauchy's integral formula and a vanishing integral lemma.

Strategy

The remainder function is defined as the n-fold iterated divided slope (swap dslope a)^[n] f. The key ingredients are:

1. dslope_expansion_identity — algebraic identity relating f to iterated dslope values.
2. iterate_dslope_differentiableOn — iterated dslope preserves differentiability on open sets, using differentiableOn_dslope from the removable singularity theory.
3. iterate_dslope_eq_iteratedDeriv_div_factorial — connects dslope coefficients to iteratedDeriv k f a / k! via formal power series machinery.

noncomputable def complexTaylorPoly (f : ℂ → ℂ) (a : ℂ) (n : ℕ) (z : ℂ) : ℂ

The complex Taylor polynomial of degree n - 1 for f centered at a: ∑_{k < n} (f^(k)(a) / k!) (z - a)^k.

theorem dslope_expansion_identity (f : ℂ → ℂ) (a z : ℂ) (n : ℕ) : f z = ∑ k ∈ Finset.range n, (Function.swap dslope a)^[k] f a * (z - a) ^ k + (Function.swap dslope a)^[n] f z * (z - a) ^ n

Algebraic identity: for any function f, point a, and evaluation point z, f(z) = ∑_{k<n} (swap dslope a)^[k] f(a) · (z-a)^k + (swap dslope a)^[n] f(z) · (z-a)^n. This is a purely algebraic consequence of the definition of dslope.

theorem iterate_dslope_differentiableOn {f : ℂ → ℂ} {Ω : Set ℂ} {a : ℂ} (hΩ : IsOpen Ω) (ha : a ∈ Ω) (hf : DifferentiableOn ℂ f Ω) (n : ℕ) : DifferentiableOn ℂ ((Function.swap dslope a)^[n] f) Ω

The n-fold iterated dslope preserves differentiability on open sets. Uses the complex removable singularity theorem (differentiableOn_dslope).

theorem iterate_dslope_eq_iteratedDeriv_div_factorial {f : ℂ → ℂ} {a : ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} (hpf : HasFPowerSeriesAt f p a) (k : ℕ) : (Function.swap dslope a)^[k] f a = iteratedDeriv k f a / ↑k.factorial

The coefficient identity: if f has a formal power series expansion at a, then the value of the k-th iterated dslope at a equals f^(k)(a) / k!.

theorem taylor_complex {f : ℂ → ℂ} {Ω : Set ℂ} {a : ℂ} (n : ℕ) (hΩ : IsOpen Ω) (ha : a ∈ Ω) (hf : DifferentiableOn ℂ f Ω) : ∃ (fₙ : ℂ → ℂ), DifferentiableOn ℂ fₙ Ω ∧ ∀ z ∈ Ω, f z = complexTaylorPoly f a n z + fₙ z * (z - a) ^ n

Taylor's Theorem (Lecture 10, Theorem 1, Part 1). If f is analytic (holomorphic) in a region Ω containing a, then for every n, $$f(z) = f(a) + \frac{f'(a)}{1!}(z-a) + \cdots + \frac{f^{(n-1)}(a)}{(n-1)!}(z-a)^{n-1}

• f_n(z)(z-a)^n,$$ where fₙ is analytic (differentiable) in Ω.

theorem circleIntegral_inv_pow_sub_mul_sub_eq_zero {a : ℂ} {R : ℝ} (hR : 0 < R) (z : ℂ) (hz : z ∈ Metric.ball a R) (n : ℕ) : ∮ (ζ : ℂ) in C(a, R), ((ζ - a) ^ (n + 1) * (ζ - z))⁻¹ = 0

Vanishing integral: ∮ 1/((ζ-a)^(n+1) * (ζ-z)) dζ = 0 for z ∈ ball(a, R) and n ≥ 0. Proved by induction on n using partial fractions and the residue computation ∮ (ζ-w)^m dζ = 0 for m ≠ -1.

theorem taylor_integral_representation {f : ℂ → ℂ} {Ω : Set ℂ} {a : ℂ} {R : ℝ} (n : ℕ) (hΩ : IsOpen Ω) (ha : a ∈ Ω) (hf : DifferentiableOn ℂ f Ω) (hR : 0 < R) (hball : Metric.closedBall a R ⊆ Ω) (z : ℂ) (hz : z ∈ Metric.ball a R) : (Function.swap dslope a)^[n] f z = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (ζ : ℂ) in C(a, R), f ζ / ((ζ - a) ^ n * (ζ - z))

Integral representation of the Taylor remainder (Lecture 10, Theorem 1, Part 2). If C is the boundary of a closed disk of radius R centered at a contained in Ω, then the remainder function fₙ satisfies $$f_n(z) = \frac{1}{2\pi i} \oint_C \frac{f(\zeta)\,d\zeta}{(\zeta - a)^n (\zeta - z)}$$ for z inside C.

The proof uses Cauchy's integral formula and induction on n. The key auxiliary result is circleIntegral_inv_pow_sub_mul_sub_eq_zero, a vanishing integral proved by partial fractions.