English
If f has a power series expansion on a ball around x with p, then around x+y, with the origin changed by y, there is a power series with radius p.radius and coefficients p.changeOriginSeries k.
Русский
Если функция имеет степенной ряд вокруг точки x, то вокруг точки x+y после переноса начала существует степенной ряд радиуса p.radius с коэффициентами p.changeOriginSeries.
LaTeX
$$$HasFPowerSeriesOnBall f p x r \\Rightarrow HasFPowerSeriesOnBall f (p.changeOrigin y) (x+y) (r-‖y‖)$$$
Lean4
/-- If a function admits a power series expansion `p` on a ball `B (x, r)`, then it also admits a
power series on any subball of this ball (even with a different center), given by `p.changeOrigin`.
-/
theorem changeOrigin (hf : HasFPowerSeriesOnBall f p x r) (h : (‖y‖₊ : ℝ≥0∞) < r) :
HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊) :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
exact hf.changeOrigin h (by simp)
