English
The tendstoUniformlyOn' variant gives uniform convergence on ball around x for the shifted partial sums p(n)(y−x).
Русский
Вариант tendstoUniformlyOn' даёт равномерную сходимость для смещённых частичных сумм p(n)(y−x) на шаре вокруг x.
LaTeX
$$$\text{tendstoUniformlyOn'} (f,p,s,x,r) : \; \text{TendstoUniformlyOn}(p.partialSum\,\cdot\, (y-x), f,\; \text{on } (\mathrm{insert}\ x\ s) \cap B(x,r))$$$
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 (x + y)` is the uniform limit of `p.partialSum n y` there. -/
theorem tendstoUniformlyOn {r' : ℝ≥0} (hf : HasFPowerSeriesWithinOnBall f p s x r) (h : (r' : ℝ≥0∞) < r) :
TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
((x + ·) ⁻¹' (insert x s) ∩ Metric.ball (0 : E) r') :=
by
obtain ⟨a, ha, C, -, 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 ^ n :=
hf.uniform_geometric_approx h
refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_
have L : Tendsto (fun n => (C : ℝ) * a ^ n) atTop (𝓝 ((C : ℝ) * 0)) :=
tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_zero_of_lt_one ha.1.le ha.2)
rw [mul_zero] at L
refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_
rw [dist_eq_norm]
exact (hp y hy.2 n hy.1).trans_lt hn
