Commit 2024-02-01 09:38 f8b99c79

feat(Analysis.Calculus.FDeriv.Analytic + Analysis.Complex.TaylorSeries): Taylor series of holomorphic functions (#10087) See here on Zulip. This adds some general lemmas due to Junyan Xu, culminating in

theorem HasFPowerSeriesOnBall.hasSum_iteratedFDeriv {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*}
    [ NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ℝ≥0∞}
    (h : HasFPowerSeriesOnBall f p x r) [CompleteSpace F] [CharZero 𝕜] {y : E} (hy : y ∈ EMetric.ball 0 r) :+1:
    HasSum (fun n ↦ (n ! : 𝕜)⁻¹• (iteratedFDeriv 𝕜 n f x) fun x ↦ y) (f (x + y))

and uses this to show that the Taylor series of a function that is complex differentiable on an open ball in ℂ converges there to the function; similarly for functions that are holomorphic on all of ℂ:

lemma Complex.hasSum_taylorSeries_on_ball {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : NNReal⦄ (hf : DifferentiableOn ℂ f (Metric.ball c ↑r)) ⦃z : ℂ⦄
    (hz : z ∈ Metric.ball c ↑r) :
    HasSum (fun n ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
lemma Complex.taylorSeries_eq_on_ball {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
    [CompleteSpace E] ⦃f : ℂ → E⦄ ⦃c : ℂ⦄ ⦃r : NNReal⦄ (hf : DifferentiableOn ℂ f (Metric.ball c ↑r)) ⦃z : ℂ⦄
    (hz : z ∈ Metric.ball c ↑r) : 
    ∑' (n : ℕ), (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z
lemma Complex.taylorSeries_eq_on_ball' ⦃c : ℂ⦄ ⦃r : NNReal⦄ ⦃z : ℂ⦄ (hz : z ∈ Metric.ball c ↑r) {f : ℂ → ℂ}
    (hf : DifferentiableOn ℂ f (Metric.ball c ↑r)) : 
    ∑' (n : ℕ), (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

and similar lemmas for EMetric.balls and entire functions.