English
If a function admits a local power-series expansion around x inside a subset s, then on a strict subdisk of its radius of convergence, the function is exponentially close to the partial sums of its power series. More precisely, there exist a real a with 0 < a < 1 and a positive constant C, such that for all small increments y with f(x+y) defined by the expansion, and for every partial sum order n, the deviation between f(x+y) and the nth partial sum is bounded by C times (a times the norm of y over the radius) raised to the n-th power.
Русский
Если функция имеет околичную разложение по степенному ряду вокруг точки x внутри множества s, то на строгом подшаре радиуса сходимости она экспоненциально близка к частичным суммам степенного ряда. Существуют a ∈ (0,1) и C > 0 такие, что для всех малых приростов y с условием определения функции и для каждого n выполняется неравенство: ‖f(x+y) − p.partialSum n y‖ ≤ C · (a · ‖y‖/r)^n.
LaTeX
$$$\\exists a \\in (0,1), \\exists C > 0, \\forall y \\in \\mathrm{MetricBall}(0, r'), \\forall n,\\; x+y \\in \\mathrm{insert}\\ x\\ s \\Rightarrow \\|f(x+y) - p.partialSum\,n\,y\\| \\le C \\,(a \\cdot (\\|y\\| / r'))^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
`HasFPowerSeriesWithinOnBall.uniform_geometric_approx` for a weaker version. -/
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 * (‖y‖ / r')) ^ n :=
by
obtain ⟨a, ha, C, hC, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ n, ‖p n‖ * (r' : ℝ) ^ n ≤ C * a ^ n :=
p.norm_mul_pow_le_mul_pow_of_lt_radius (h.trans_le hf.r_le)
refine ⟨a, ha, C / (1 - a), div_pos hC (sub_pos.2 ha.2), fun y hy n ys => ?_⟩
have yr' : ‖y‖ < r' := by
rw [ball_zero_eq] at hy
exact hy
have hr'0 : 0 < (r' : ℝ) := (norm_nonneg _).trans_lt yr'
have : y ∈ EMetric.ball (0 : E) r :=
by
refine mem_emetric_ball_zero_iff.2 (lt_trans ?_ h)
simpa [enorm] using yr'
rw [norm_sub_rev, ← mul_div_right_comm]
have ya : a * (‖y‖ / ↑r') ≤ a := mul_le_of_le_one_right ha.1.le (div_le_one_of_le₀ yr'.le r'.coe_nonneg)
suffices ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / r')) ^ n / (1 - a * (‖y‖ / r'))
by
refine this.trans ?_
have : 0 < a := ha.1
gcongr
apply_rules [sub_pos.2, ha.2]
apply norm_sub_le_of_geometric_bound_of_hasSum (ya.trans_lt ha.2) _ (hf.hasSum ys this)
intro n
calc
‖(p n) fun _ : Fin n => y‖
_ ≤ ‖p n‖ * ∏ _i : Fin n, ‖y‖ := (ContinuousMultilinearMap.le_opNorm _ _)
_ = ‖p n‖ * (r' : ℝ) ^ n * (‖y‖ / r') ^ n := by simp [field, div_pow]
_ ≤ C * a ^ n * (‖y‖ / r') ^ n := by gcongr ?_ * _; apply hp
_ ≤ C * (a * (‖y‖ / r')) ^ n := by rw [mul_pow, mul_assoc]
