English
For a differentiable f on an emetric ball, the Taylor expansion holds exactly as in the standard metric setting.
Русский
Для функции, дифференцируемой на эмитрическом шаре, разложение Тейлора выполняется точно так же, как в обычной метрике.
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_emetric_ball' {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (EMetric.ball c r)) :
∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z :=
by
convert taylorSeries_eq_on_emetric_ball hf hz using 3 with n
rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]
