English
If a function has a formal power-series representation within a set on a ball, then for any radius r' less than the ball radius, the same kind of geometric estimate holds without the s-subset refinement: the remainder is controlled by a geometric factor in n, uniformly over y in the ball.
Русский
Если функция имеет формальное степенное представление внутри множества на шаре, то для любого r' меньше радиуса шара сохраняется геометрическое оценивание остатка: остаток контролируется геометрическим множителем в n, равномерно по y внутри шара.
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 within a set in a ball, then it is exponentially
close to the partial sums of this power series on strict subdisks of the disk of convergence. -/
theorem uniform_geometric_approx {r' : ℝ≥0} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
∃ a ∈ Ioo (0 : ℝ) 1,
∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n, x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n :=
by
obtain ⟨a, ha, C, hC, hp⟩ :
∃ a ∈ Ioo (0 : ℝ) 1,
∃ C > 0,
∀ y ∈ Metric.ball (0 : E) r',
∀ n, x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * (a * (‖y‖ / r')) ^ n :=
hf.uniform_geometric_approx' h
refine ⟨a, ha, C, hC, fun y hy n ys => (hp y hy n ys).trans ?_⟩
have yr' : ‖y‖ < r' := by rwa [ball_zero_eq] at hy
have := ha.1.le
gcongr
exact mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.coe_nonneg)
