English
If the abscissa of absolute convergence of f is finite, then LSeries f x tends to f(1) as x → ∞.
Русский
Если абсцисса абсолютной сходимости f конечна, то LSeries f x стремится к f(1) при x → ∞.
LaTeX
$$$$ \operatorname{abscissaOfAbsConv}(f) < \infty \quad\Rightarrow\quad \lim_{x \to \infty} \mathrm{LSeries} f x = f(1). $$$$
Lean4
/-- If the L-series of `f` converges at some point, then `f 1` is the limit of `LSeries f x`
as `x → ∞`. -/
theorem tendsto_atTop {f : ℕ → ℂ} (ha : abscissaOfAbsConv f < ⊤) :
Tendsto (fun x : ℝ ↦ LSeries f x) atTop (nhds (f 1)) :=
by
let F (n : ℕ) : ℂ := if n = 0 then 0 else f n
have hF₀ : F 0 = 0 := rfl
have hF {n : ℕ} (hn : n ≠ 0) : F n = f n := if_neg hn
have ha' : abscissaOfAbsConv F < ⊤ := (abscissaOfAbsConv_congr hF).symm ▸ ha
simp_rw [← LSeries_congr hF]
convert LSeries.tendsto_cpow_mul_atTop (n := 0) (fun _ hm ↦ Nat.le_zero.mp hm ▸ hF₀) ha' using 1
simp
