Theorems · Theorem · number theory

LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq

∀ {f g : ℕ → ℂ},
  LSeries.abscissaOfAbsConv f < ⊤ →
    LSeries.abscissaOfAbsConv g < ⊤ →
      ((fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x) →
        (fun x => LSeries (f - g) ↑x) =ᶠ[Filter.atTop] 0

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.

Defined in

Mathlib.NumberTheory.LSeries.Injectivity

Cited by

1 results in Mathlib

Foundations

Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound