English
If the L-series of f and g converge and they agree for large real arguments, then the L-series of f − g is eventually zero.
Русский
Если L-серии f и g сходятся и совпадают на больших значениях реальных аргументов, тогда L-серия f − g равна нулю для больших аргументов.
LaTeX
$$$$ \text{If } hf,hg < \top \text{ and } (LSeries f)(x) = (LSeries g)(x) \text{ for large } x, \text{ then } (LSeries (f-g))(x) = 0 \text{ for large } x. $$$$
Lean4
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then the L-series of `f - g` is zero for large real arguments. -/
theorem LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq {f g : ℕ → ℂ} (hf : abscissaOfAbsConv f < ⊤)
(hg : abscissaOfAbsConv g < ⊤) (h : (fun x : ℝ ↦ LSeries f x) =ᶠ[atTop] fun x ↦ LSeries g x) :
(fun x : ℝ ↦ LSeries (f - g) x) =ᶠ[atTop] (0 : ℝ → ℂ) :=
by
rw [EventuallyEq, eventually_atTop] at h ⊢
obtain ⟨x₀, hx₀⟩ := h
obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf
obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
have Hf : LSeriesSummable f x :=
by
refine
LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx
have Hg : LSeriesSummable g x :=
by
refine
LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
exact (le_max_right yf _).trans <| (le_max_right x₀ _).trans hx
rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
