English
If HasFPowerSeriesOnBall f pf x r holds, then HasFPowerSeriesOnBall (fun y => z + f y (y - x)) (pf.unshift z) x r holds as well.
Русский
Если существует разложение в шаре для f вокруг x, то для функции g(y) = z + f(y)(y - x) существует разложение вокруг x с коэффициентами pf.unshift z.
LaTeX
$$HasFPowerSeriesOnBall f pf x r → HasFPowerSeriesOnBall (λ y, z + f y (y - x)) (pf.unshift z) x r$$
Lean4
theorem unshift (hf : HasFPowerSeriesOnBall f pf x r) :
HasFPowerSeriesOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) x r
where
r_le := by
rw [FormalMultilinearSeries.radius_unshift]
exact hf.r_le
r_pos := hf.r_pos
hasSum := by
intro y hy
apply HasSum.zero_add
simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one, continuousMultilinearCurryRightEquiv_symm_apply',
add_sub_cancel_left]
exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy)
