English
If f has a formal power series within ball, then the image-sub deriv bound holds uniformly for pairs (y,z) in the ball around (x,x).
Русский
Если f имеет формальное степенное разложение в шаре, то ограничение остатка на пары (y,z) в шаре около (x,x) сохраняется равномерно.
LaTeX
$$$\|f(y) - f(z) - p(1)(y-z)\| \le C \cdot \max\|y-x\| \|z-x\| \cdot \|y-z\|$ для \; y,z$$
Lean4
/-- If a function admits a power series expansion within a set at `x`, then it is the locally
uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f y`
is the locally uniform limit of `p.partialSum n (y - x)` there. -/
theorem tendstoLocallyUniformlyOn' (hf : HasFPowerSeriesWithinOnBall f p s x r) :
TendstoLocallyUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (insert x s ∩ EMetric.ball (x : E) r) :=
by
have A : ContinuousOn (fun y : E => y - x) (insert x s ∩ EMetric.ball (x : E) r) :=
(continuous_id.sub continuous_const).continuousOn
convert hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1
· ext z
simp
· intro z
simp [edist_eq_enorm_sub]
