English
If f has a finite power series on a ball around x with radius r, then the translated function z ↦ f(z − y) has the same finite power series around x + y with the same order and radius.
Русский
Если у функции f есть конечный степенной ряд на окружности радиуса r вокруг точки x, то преобразование z ↦ f(z − y) имеет такой же конечный степенной ряд вокруг точки x + y с тем же порядком и радиусом.
LaTeX
$$$\forall f,p,E,F,x,n,r,y:\ HasFiniteFPowerSeriesOnBall\ f\ p\ x\ n\ r \Rightarrow HasFiniteFPowerSeriesOnBall\ (fun z => f (z - y))\ p\ (x + y)\ n\ r.$$$
Lean4
/-- If a function `f` has a finite power series `p` around `x`, then the function
`z ↦ f (z - y)` has the same finite power series around `x + y`. -/
theorem comp_sub (hf : HasFiniteFPowerSeriesOnBall f p x n r) (y : E) :
HasFiniteFPowerSeriesOnBall (fun z => f (z - y)) p (x + y) n r :=
⟨hf.1.comp_sub y, hf.finite⟩
