Locally uniform Dirichlet-series convergence from signed partial-sum growth

Proved

ordered_dirichlet_series_locally_uniform_of_partial_sum_bound

by ryanshin · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorydirichlet-seriesformalizationriemann-hypothesis

Let $f:\mathbb N\to\mathbb C$ and $r\ge0$ , and assume $M(N)=\sum_{n=1}^Nf(n)=O(N^r)$ . Put $F(s)=s\int_1^\infty M(\lfloor t\rfloor)t^{-s-1}\,dt$ . Then

\sum_{n=1}^Nf(n)n^{-s}\longrightarrow F(s)\quad\text{locally uniformly on }\operatorname{Re}s>r.

In particular the convergence is uniform on each compact subset of that half-plane. Uniformity on the entire unbounded half-plane is not asserted. This stronger mode of convergence supports holomorphic limit arguments and differentiation.

Preamble

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.NumberTheory.LSeries.Dirichlet
import Mathlib.NumberTheory.LSeries.SumCoeff
import Mathlib.Analysis.MellinTransform
import Mathlib.Tactic.NormNum
open MeasureTheory
open scoped Topology

Formal statement

theorem ordered_dirichlet_series_locally_uniform_of_partial_sum_bound
    (f : ℕ → ℂ) {r : ℝ} (hr : 0 ≤ r)
    (hO : Asymptotics.IsBigO Filter.atTop
      (fun N : ℕ => ∑ n ∈ Finset.Icc 1 N, f n)
      (fun N : ℕ => (N : ℝ) ^ r)) :
    TendstoLocallyUniformlyOn
      (fun N : ℕ => fun s : ℂ => ∑ n ∈ Finset.Icc 1 N, f n / (n : ℂ) ^ s)
      (fun s : ℂ => s * mellin (fun t : ℝ => ∑ n ∈ Finset.Icc 1 ⌊t⌋₊, f n) (-s))
      Filter.atTop {s : ℂ | r < s.re} := by sorry

Source

Quantitative corollary proved from pinned Mathlib https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/NumberTheory/AbelSummation.lean#L229, sum_mul_eq_sub_integral_mul₀', and https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean#L172, integral_Ioi_rpow_of_lt. The explicit resulting error bound is uniform on each set Re(s)>=sigma>r, |s|<=R.

View graph