English
The tendstoUniformlyOn' version shows uniform convergence of partial sums on a ball with y−x substitution.
Русский
Версия tendstoUniformlyOn' демонстрирует равномерную сходимость частичных сумм на шаре с заменой y−x.
LaTeX
$$$\text{tendstoUniformlyOn'} (hf,h) : \; \text{TendstoUniformlyOn}(p.partialSum n (y-x))$$$$
Lean4
/-- If a function admits a power series expansion within a set at `x`, then it is the locally
uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
is the locally uniform limit of `p.partialSum n y` there. -/
theorem tendstoLocallyUniformlyOn (hf : HasFPowerSeriesWithinOnBall f p s x r) :
TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop
((x + ·) ⁻¹' (insert x s) ∩ EMetric.ball (0 : E) r) :=
by
intro u hu y hy
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩
have : EMetric.ball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds EMetric.isOpen_ball yr'
refine ⟨(x + ·) ⁻¹' (insert x s) ∩ EMetric.ball (0 : E) r', ?_, ?_⟩
· rw [nhdsWithin_inter_of_mem']
· exact inter_mem_nhdsWithin _ this
· apply mem_nhdsWithin_of_mem_nhds
apply Filter.mem_of_superset this (EMetric.ball_subset_ball hr'.le)
· simpa [Metric.emetric_ball_nnreal] using hf.tendstoUniformlyOn hr' u hu
