abscissaOfAbsConv_congr' — Mathlib

English

If f and g are eventually equal (f =ᶠ[atTop] g), then their abscissae of absolute convergence are equal: abscissaOfAbsConv f = abscissaOfAbsConv g.

Русский

Если f и g сходятся вплоть до больших значений, то их абсциссы абсолютной сходимости совпадают.

LaTeX

$$$\\forall f,g:\\mathbb{N}\\to\\mathbb{C},\\; f =^\\infty_{\\text{atTop}} g \\Rightarrow \\operatorname{abscissaOfAbsConv}(f)=\\operatorname{abscissaOfAbsConv}(g).$$$

Lean4

/-- If `f` and `g` agree on large `n : ℕ`, then their `LSeries` have the same
abscissa of absolute convergence. -/
theorem abscissaOfAbsConv_congr' {f g : ℕ → ℂ} (h : f =ᶠ[atTop] g) : abscissaOfAbsConv f = abscissaOfAbsConv g :=
  congr_arg sInf <| congr_arg _ <| Set.ext fun x ↦ LSeriesSummable_congr' x h

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