English
If a function has a power-series expansion about x on a ball of radius r, then for any r' strictly smaller than r there exist a ∈ (0,1) and C > 0 such that the difference between f(x+y) and its nth partial sum is bounded by C times a^n for all y in the ball of radius r'.
Русский
Если функция имеет степенной ряд вокруг x на шаре радиуса r, то для любого r' < r существуют a ∈ (0,1) и C > 0 такие, что разность между f(x+y) и n-й частичной суммой ограничена C·a^n для всех y в шаре радиуса r'.
LaTeX
$$$\exists a \in Ioo(0,1), \exists C > 0, \forall y \in \mathrm{MetricBall}(0,r'), \forall n, \|f(x+y) - p.partialSum\,n\,y\| \le C \; a^n$$$
Lean4
/-- If a function admits a power series expansion, then it is exponentially close to the partial
sums of this power series on strict subdisks of the disk of convergence.
This version provides an upper estimate that decreases both in `‖y‖` and `n`. See also
`HasFPowerSeriesOnBall.uniform_geometric_approx` for a weaker version. -/
theorem uniform_geometric_approx' {r' : ℝ≥0} (hf : HasFPowerSeriesOnBall f p x r) (h : (r' : ℝ≥0∞) < r) :
∃ a ∈ Ioo (0 : ℝ) 1,
∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
simpa using hf.uniform_geometric_approx' h
