English
If f is differentiable, then around any center z, there is a power series representation for f that converges everywhere with radius ∞.
Русский
Если f дифференцируема, то вокруг любой точки z существует степенной ряд, сходящийся на всей плоскости.
LaTeX
$$HasFPowerSeriesOnBall f (cauchyPowerSeries f z R) z ∞$$
Lean4
/-- When `f : ℂ → E` is differentiable, the `cauchyPowerSeries f z R` represents `f` as a power
series centered at `z` in the entirety of `ℂ`, regardless of `R : ℝ≥0`, with `0 < R`. -/
protected theorem _root_.Differentiable.hasFPowerSeriesOnBall {f : ℂ → E} (h : Differentiable ℂ f) (z : ℂ) {R : ℝ≥0}
(hR : 0 < R) : HasFPowerSeriesOnBall f (cauchyPowerSeries f z R) z ∞ :=
(h.differentiableOn.hasFPowerSeriesOnBall hR).r_eq_top_of_exists fun _r hr =>
⟨_, h.differentiableOn.hasFPowerSeriesOnBall hr⟩
