English
If L-series of f and g converge and are eventually equal, then f(n) = g(n) for all n ≠ 0.
Русский
Если L-серии f и g сходятся и совпадают для больших n, тогда f(n) = g(n) для всех n ≠ 0.
LaTeX
$$$$ \text{If } hf,hg < \top \text{ and } (LSeries f) =^{\!\!\to}_{atTop} (LSeries g) \Rightarrow \forall n \neq 0, \; f(n)=g(n). $$$$
Lean4
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then `f n = g n` whenever `n ≠ 0`. -/
theorem eq_of_LSeries_eventually_eq {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤) (hg : abscissaOfAbsConv g < ⊤)
(h : (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] fun x ↦ LSeries g x) {n : ℕ} (hn : n ≠ 0) : f n = g n :=
by
have hsub : (fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq hf hg h
have ha : abscissaOfAbsConv (f - g) ≠ ⊤ :=
lt_top_iff_ne_top.mp <| (abscissaOfAbsConv_sub_le f g).trans_lt <| max_lt hf hg
simpa only [Pi.sub_apply, sub_eq_zero] using (LSeries_eventually_eq_zero_iff'.mp hsub).resolve_right ha n hn
