taylorSeries_eq_on_emetric_ball — Mathlib

English

If f is differentiable on the whole complex plane, then the same Taylor expansion holds with the global HasSum formula for any center c and z.

Русский

Если f дифференцируема на всей плоскости, то формула разложения Тейлора справедлива глобально для любого центра и точки.

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 : ∑' n : ℕ, (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c = f z :=
  (hasSum_taylorSeries_on_emetric_ball hf hz).tsum_eq

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