English
If both f and g have finite abscissa of absolute convergence, then LSeries f = LSeries g if and only if f(n) = g(n) for all n ≠ 0.
Русский
Если обе функции f и g имеют конечную абсциссу абсолютной сходимости, то LSeries f = LSeries g тогда и только тогда, когда f(n) = g(n) для всех n ≠ 0.
LaTeX
$$$$ \operatorname{abscissaOfAbsConv}(f) < \top \quad\land\quad \operatorname{abscissaOfAbsConv}(g) < \top \;\Rightarrow\; LSeries f = LSeries g \iff \forall n \neq 0, \; f(n)=g(n). $$$$
Lean4
/-- If the `LSeries` of `f` and of `g` both converge somewhere, then they are equal if and only
if `f n = g n` whenever `n ≠ 0`. -/
theorem LSeries_eq_iff_of_abscissaOfAbsConv_lt_top {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤)
(hg : abscissaOfAbsConv g < ⊤) : LSeries f = LSeries g ↔ ∀ n ≠ 0, f n = g n :=
by
refine ⟨fun H n hn ↦ ?_, fun H ↦ funext (LSeries_congr fun {n} ↦ H n)⟩
refine eq_of_LSeries_eventually_eq hf hg ?_ hn
exact Filter.Eventually.of_forall fun x ↦ congr_fun H x
