English
For HasFPowerSeriesWithinOnBall hf, the image_sub_sub_deriv_principal expresses a uniform bound for the remainder when comparing f(y1) and f(y2).
Русский
Для HasFPowerSeriesWithinOnBall hf выражено единообразное ограничение остатка при сравнении f(y1) и f(y2).
LaTeX
$$$\exists C>0, \forall y_1,y_2 \in ... : \| f(y_1) - f(y_2) - p(1)(y_1-y_2)\| \le C \cdot \max\|y_1-x\| \|y_2-x\| \cdot \|y_1-y_2\|$$$
Lean4
/-- If a function admits a power series expansion within a set at `x`, then it is the uniform limit
of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
is the uniform limit of `p.partialSum n (y - x)` there. -/
theorem tendstoUniformlyOn' {r' : ℝ≥0} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.ball (x : E) r') :=
by
convert (hf.tendstoUniformlyOn h).comp fun y => y - x using 1
· simp [Function.comp_def]
· ext z
simp [dist_eq_norm]
