English
Let f be a function such that the Abel summation sequence tends to l. Then for every z with |z|<1 a certain transformed tail-sum series converges to l − ∑ f(n) z^n.
Русский
Пусть f удовлетворяет условиям Абеля: последовательность Абеля сходится к l; тогда преобразованная хвостовая сумма сходится к l − ∑ f(n) z^n.
LaTeX
$$$$\\text{If } h: \\operatorname{Tendsto}\\left(n \\mapsto \\sum_{i=0}^{n-1} f(i)\\right)_{\\mathrm{atTop}} (\\mathcal{N} l) \\text{ and } |z|<1, \\\\ \\operatorname{Tendsto}\\left(n \\mapsto (1 - z) \\sum_{i=0}^{n-1} \\left(l - \\sum_{j=0}^{i} f(j)\\right) z^{i}\\right)_{\\mathrm{atTop}} (\\mathcal{N} \\left(l - \\sum_{n=0}^{\\infty} f(n) z^{n}\\right)).$$$$
Lean4
theorem isOpen_setOf_mem_nhds_and_isMaxOn_norm {f : E → F} {s : Set E} (hd : DifferentiableOn ℂ f s) :
IsOpen {z | s ∈ 𝓝 z ∧ IsMaxOn (norm ∘ f) s z} :=
by
refine isOpen_iff_mem_nhds.2 fun z hz => (eventually_eventually_nhds.2 hz.1).and ?_
replace hd : ∀ᶠ w in 𝓝 z, DifferentiableAt ℂ f w := hd.eventually_differentiableAt hz.1
exact (norm_eventually_eq_of_isLocalMax hd <| hz.2.isLocalMax hz.1).mono fun x hx y hy => le_trans (hz.2 hy).out hx.ge
