LSeriesSummable_congr' — Mathlib

English

If f and g agree eventually, then L-series summability at s for f is equivalent to that for g.

Русский

Если f и g совпадают на бесконечно больших n, то суммируемость L-серии в s для f эквивалентна суммируемости для g.

LaTeX

$$$(\exists N \in \mathbb{N}, \forall n \ge N, f(n)=g(n)) \Rightarrow \bigl( LSeriesSummable(f,s) \Leftrightarrow LSeriesSummable(g,s) \bigr)$$$

Lean4

/-- If `f` and `g` agree on large `n : ℕ`, then the `LSeries` of `f` converges at `s`
if and only if that of `g` does. -/
theorem LSeriesSummable_congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g) : LSeriesSummable f s ↔ LSeriesSummable g s :=
  ⟨fun H ↦ H.congr' s h, fun H ↦ H.congr' s h.symm⟩

Похожие утверждения