English
Analyticity holds for all k, provided a positive radius, by applying the power-series-with-origin-change construction.
Русский
Аналитичность сохраняется при любых k, при условии положительного радиуса, с использованием конструкции переноса начала.
LaTeX
$$$\\text{AnalyticAt } 𝕜 (p.changeOrigin x k) 0$ for all k, when p.radius>0$$
Lean4
/-- If a function admits a power series expansion `p` within a set `s` on a ball `B (x, r)`, then
it also admits a power series on any subball of this ball (even with a different center provided
it belongs to `s`), given by `p.changeOrigin`. -/
theorem changeOrigin (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : ‖y‖ₑ < r) (hy : x + y ∈ insert x s) :
HasFPowerSeriesWithinOnBall f (p.changeOrigin y) s (x + y) (r - ‖y‖ₑ)
where
r_le := by
apply le_trans _ p.changeOrigin_radius
exact tsub_le_tsub hf.r_le le_rfl
r_pos := by simp [h]
hasSum {z} h'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 (hz.trans_le hf.r_le), add_assoc, hf.sum]
· have : insert (x + y) s ⊆ insert (x + y) (insert x s) := by apply insert_subset_insert (subset_insert _ _)
rw [insert_eq_of_mem hy] at this
apply this
simpa [add_assoc] using h'z
exact mem_emetric_ball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)
rw [this]
apply (p.changeOrigin y).hasSum
refine EMetric.ball_subset_ball (le_trans ?_ p.changeOrigin_radius) hz
exact tsub_le_tsub hf.r_le le_rfl
