English
For an emetric ball around c of radius r, the Taylor series equality holds with HasSum as in the non-emetric case.
Русский
Для эмитрического шара вокруг c радиуса r равенство ряда Тейлора сохраняется через HasSum аналогично обычному случаю.
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 hasSum_taylorSeries_on_emetric_ball :
HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z) :=
by
obtain ⟨r', hzr', hr'⟩ := exists_between (EMetric.mem_ball'.mp hz)
lift r' to NNReal using ne_top_of_lt hr'
rw [← EMetric.mem_ball', Metric.emetric_ball_nnreal] at hzr'
refine hasSum_taylorSeries_on_ball ?_ hzr'
rw [← Metric.emetric_ball_nnreal]
exact hf.mono <| EMetric.ball_subset_ball hr'.le
