taylorSeries_eq_on_ball — Mathlib

English

As above, with the same hypothesis, for every z in the ball B(c, r) one has the Taylor series formula f(z) = ∑ (z−c)^n/n! · iteratedDeriv_n f(c).

Русский

Так же, как и выше, для каждого z внутри шарa B(c, r) выполняется формула ряда Тейлора.

LaTeX

$$$\sum_{n=0}^\infty \frac{(z - c)^n}{n!} \; \operatorname{iteratedDeriv}_n f(c) = 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 : ∑' n : ℕ, (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z :=
  (hasSum_taylorSeries_on_ball hf hz).tsum_eq

Похожие утверждения