English
If a power series within a ball exists for f, then the shifted function y ↦ z + f(y)(y − x) also has a power series within a ball with the shifted coefficients pf.unshift z.
Русский
Если для функции f есть ряд до окружности внутри шара, то сдвинутая функция y ↦ z + f(y)(y − x) имеет ряд в шаре с сдвинутыми коэффициентами pf.unshift z.
LaTeX
$$HasFPowerSeriesWithinOnBall f pf s x r → HasFPowerSeriesWithinOnBall (λ y, z + f y (y - x)) (pf.unshift z) s x r$$
Lean4
theorem unshift (hf : HasFPowerSeriesWithinOnBall f pf s x r) :
HasFPowerSeriesWithinOnBall (fun y ↦ z + f y (y - x)) (pf.unshift z) s x r
where
r_le := by
rw [FormalMultilinearSeries.radius_unshift]
exact hf.r_le
r_pos := hf.r_pos
hasSum := by
intro y hy h'y
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 h'y)
