English
If a function has a power-series around x within a set, then it is locally uniformly convergent to its partial sums on subdomains near x.
Русский
Если функция имеет степенной ряд вокруг x внутри множества, то частичные суммы сходятся равномерно локально на поддомены рядом с x.
LaTeX
$$$\text{tendstoLocallyUniformlyOn} \; (f,p,s,x) : \text{...}$$$
Lean4
/-- If `f` has formal power series `∑ n, pₙ` at `x`, then
`f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`.
In particular, `f` is strictly differentiable at `x`. -/
theorem isBigO_image_sub_norm_mul_norm_sub (hf : HasFPowerSeriesAt f p x) :
(fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓝 (x, x)] fun y => ‖y - (x, x)‖ * ‖y.1 - y.2‖ :=
by
rw [← hasFPowerSeriesWithinAt_univ] at hf
simpa using hf.isBigO_image_sub_norm_mul_norm_sub
