taylorSeries_eq_of_entire' — Mathlib

English

If f is differentiable on the complex plane, then f(z) equals the Taylor series around any center c, i.e., f(z) = ∑ (z−c)^n/n! · iteratedDeriv_n f(c).

Русский

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

LaTeX

$$$\sum_{n=0}^{\infty} (z - c)^n / n! \cdot \operatorname{iteratedDeriv}_n f(c) = f(z)$$$

Lean4

/-- A function that is complex differentiable on the complex plane is given by evaluating
its Taylor series at any point `c`. -/
theorem taylorSeries_eq_of_entire' {f : ℂ → ℂ} (hf : Differentiable ℂ f) :
    ∑' n : ℕ, (n ! : ℂ)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z :=
  by
  convert taylorSeries_eq_of_entire hf c z using 3 with n
  rw [mul_right_comm, smul_eq_mul, smul_eq_mul, mul_assoc]

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