English
If f has a power series p about x on s with radius r, then the translated function z ↦ f(z−y) has the same power series p about x+y on s+{y} with radius r.
Русский
Если у функции f есть степенной ряд p около x на s радиуса r, то через преобразование z↦f(z−y) имеет тот же ряд p около x+y на s+{y} радиуса r.
LaTeX
$$$HasFPowerSeriesWithinOnBall\ f\ p\ s\ x\ r \Rightarrow HasFPowerSeriesWithinOnBall\ (\\fun z \\to f (z - y))\ p\ (s + { y })\ (x + y)\ r$$$
Lean4
theorem comp_sub (hf : HasFPowerSeriesWithinOnBall f p s x r) (y : E) :
HasFPowerSeriesWithinOnBall (fun z ↦ f (z - y)) p (s + { y }) (x + y) r
where
r_le := hf.r_le
r_pos := hf.r_pos
hasSum {z} hz1
hz2 :=
by
have : x + z ∈ insert x s :=
by
simp only [add_singleton, image_add_right, mem_insert_iff, add_eq_left, mem_preimage] at hz1 ⊢
abel_nf at hz1
assumption
convert hf.hasSum this hz2 using 2
abel
