English
If a function has a power-series expansion within a ball, then it is continuous there, as the partial-sum approximants converge uniformly on compact sets to the function.
Русский
Если функция имеет степенной ряд в шаре, то она непрерывна там: частичные суммы сходятся равномерно на компактах к функции.
LaTeX
$$$\text{HasFPowerSeriesWithinOnBall}(f,p,s,x,r) \Rightarrow \text{ContinuousWithinOnBall}(f,(s,x),r)$$$
Lean4
/-- If `f` has formal power series `∑ n, pₙ` on a ball of radius `r`, then for `y, z` in any smaller
ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above by
`C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. -/
theorem image_sub_sub_deriv_le (hf : HasFPowerSeriesOnBall f p x r) (hr : r' < r) :
∃ C,
∀ᵉ (y ∈ EMetric.ball x r') (z ∈ EMetric.ball x r'),
‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖ :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
simpa only [mem_univ, insert_eq_of_mem, univ_inter] using hf.image_sub_sub_deriv_le hr
