Theorems · Theorem · number theory

LSeries.tendsto_cpow_mul_atTop

∀ {f : ℕ → ℂ} {n : ℕ},
  (∀ m ≤ n, f m = 0) →
    LSeries.abscissaOfAbsConv f < ⊤ →
      Filter.Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) Filter.atTop (nhds (f (n + 1)))

If the coefficients f m of an L-series are zero for m ≤ n and the L-series converges at some point, then f (n+1) is the limit of (n+1)^x * LSeries f x as x → ∞.

Defined in

Mathlib.NumberTheory.LSeries.Injectivity

Cited by

2 results in Mathlib

Foundations

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