English
The map sending a pair (p, q) to q.snd.compContinuousLinearMap p.fst is analytic on the relevant product, i.e., it is an analytic function of the pair.
Русский
Отображение, отправляющее пару (p, q) в q.snd.compContinuousLinearMap p.fst, является аналитическим на соответствующем произведении.
LaTeX
$$$AnalyticOn\ 𝕜\ (\lambda p \mapsto p.\mathrm{snd}.\mathrm{compContinuousLinearMap} p.\mathrm{fst})\ t$$$
Lean4
/-- If a function admits a power series expansion 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 : HasFPowerSeriesOnBall f p x r) :
TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) atTop (EMetric.ball (0 : E) r) :=
by
rw [← hasFPowerSeriesWithinOnBall_univ] at hf
simpa using hf.tendstoLocallyUniformlyOn
