English
If a finite power-series on a ball exists, then a change of origin yields a new finite power-series on a translated ball with appropriately reduced radius.
Русский
Если существует конечная степенная серия на шаре, то смена начала координат даёт новую конечную степенную серию на перенесённом шаре с уменьшенной радиусом.
LaTeX
$$HasFiniteFPowerSeriesOnBall f p x n r → HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ‖y‖₊)$$
Lean4
theorem changeOrigin (hf : HasFiniteFPowerSeriesOnBall f p x n r) (h : (‖y‖₊ : ℝ≥0∞) < r) :
HasFiniteFPowerSeriesOnBall f (p.changeOrigin y) (x + y) n (r - ‖y‖₊)
where
r_le := (tsub_le_tsub_right hf.r_le _).trans p.changeOrigin_radius
r_pos := by simp [h]
finite _ hm := p.changeOrigin_finite_of_finite hf.finite hm
hasSum {z}
hz :=
by
have : f (x + y + z) = FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z :=
by
rw [mem_emetric_ball_zero_iff, lt_tsub_iff_right, add_comm] at hz
rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]
exact mem_emetric_ball_zero_iff.2 ((enorm_add_le _ _).trans_lt hz)
rw [this]
apply (p.changeOrigin y).hasSum_of_finite fun _ => p.changeOrigin_finite_of_finite hf.finite
