English
If f is differentiable on the emetric ball around c with radius r, then the Taylor series expansion around c converges to f(z) for z in that emetric ball.
Русский
Если f дифференцируема на эмитрическом шаре вокруг c радиуса r, разложение Тейлора вокруг c сходится к f(z) для z в этом эмитрическом шаре.
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 taylorSeries_eq_on_ball' {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball c r)) :
∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z :=
by
convert taylorSeries_eq_on_ball hf hz using 3 with n
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
