English
Let f,g : ℕ → ℂ. If f and g agree for all sufficiently large n and the L-series of f converges at s, then the L-series of g converges at s.
Русский
Пусть f,g : ℕ → ℂ. Если f и g совпадают для всех достаточно больших n и L-серия f сходится в точке s, то и L-серия g сходится в точке s.
LaTeX
$$$\Big( \exists N \in \mathbb{N}, \forall n \ge N, f(n)=g(n) \Big) \Rightarrow \bigl( LSeriesSummable(f,s) \Rightarrow LSeriesSummable(g,s) \bigr)$$
Lean4
/-- If `f` and `g` agree on large `n : ℕ` and the `LSeries` of `f` converges at `s`,
then so does that of `g`. -/
theorem congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g) (hf : LSeriesSummable f s) : LSeriesSummable g s :=
by
rw [← Nat.cofinite_eq_atTop] at h
refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually ?_
have : term f s =ᶠ[cofinite] term g s :=
by
rw [eventuallyEq_iff_exists_mem] at h ⊢
obtain ⟨S, hS, hS'⟩ := h
refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
rw [Set.mem_diff, Set.mem_singleton_iff] at hn
simp [hn.2, hS' hn.1]
exact this.symm.mono fun n hn ↦ by simp [hn]
