English
For a differentiable f on ball B(c, r) with r > 0, and any z in that ball, f(z) is given by its Taylor series around c: f(z) = ∑_{n≥0} (z−c)^n/n! · iteratedDeriv_n f(c).
Русский
Для дифференцируемой функции f на шаре B(c, r) с r > 0 и любого z внутри шара, f(z) равняется сумме ряда Тейлора: f(z) = ∑ (z−c)^n / n! · iteratedDeriv_n f(c).
LaTeX
$$$\text{HasSum}\left(\sum_{n=0}^\infty \frac{(z - c)^n}{n!} \; \operatorname{iteratedDeriv}_n f(c)\right) = f(z)$$$
Lean4
/-- 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 hasSum_taylorSeries_on_ball : HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z) :=
by
obtain ⟨r', hr', hr'₀, hzr'⟩ : ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r' :=
by
obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩
lift r' to NNReal using hr'₀.le
have hz' : z - c ∈ EMetric.ball 0 r' := by
rw [Metric.emetric_ball_nnreal]
exact mem_ball_zero_iff.mpr hzr'
have H := (hf.mono <| Metric.closedBall_subset_ball hr').hasFPowerSeriesOnBall hr'₀ |>.hasSum_iteratedFDeriv hz'
simp only [add_sub_cancel] at H
convert H using 4 with n
simpa only [iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, mul_one, Finset.prod_const, Finset.card_fin] using
((iteratedFDeriv ℂ n f c).map_smul_univ (fun _ ↦ z - c) (fun _ ↦ 1)).symm
