English
If f has a formal multilinear power series about x, then the difference quotient approximates the linear term in a uniform way near (x,x).
Русский
Если f имеет формальное многолинейное разложение около x, то разности деление приближают линейный член в окрестности (x,x).
LaTeX
$$$f(y) - f(z) - p(1)(y-z) = O(\|y-z\|)$ as y,z → x$$
Lean4
/-- If a function admits a power series expansion 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 : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f atTop (Metric.ball (x : E) r') :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
simpa using hf.tendstoUniformlyOn' h
