Prove2Me

The residue at s=1s=1 equals the average of the Dirichlet coefficients

Proved
ClassNumberFormula.residue_eq_average_of_coefficients

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

class-number-formulanumber-theory

Let (an)n≥1(a_n)_{n\ge1} be a sequence of non-negative real numbers whose averages converge:

lim⁡N→∞1N∑n=1Nan=ρ.\lim_{N\to\infty}\frac1N\sum_{n=1}^N a_n = \rho .

Then the Dirichlet series L(s)=∑n≥1ann−sL(s) = \sum_{n\ge1} a_n n^{-s} satisfies

lim⁡s→1+(s−1) L(s)=ρ.\lim_{s\to1^+}(s-1)\,L(s) = \rho .

Applied to the coefficients of the Dedekind zeta function (which count ideals and are non-negative), this reduces the residue of ζK\zeta_K at s=1s=1 to the average number of ideals of norm at most NN.

Formalization Note The limit is taken along real s→1+s \to 1^+. Non-negativity is the setting of the source (the coefficients are counts); it guarantees absolute convergence of L(s)L(s) for real s>1s > 1, which Mathlib's LSeries (a tsum) needs in order to be meaningful.

Preamble
import Mathlib
open NumberField NumberField.InfinitePlace NumberField.Units Filter Topology Real
Formal statement
namespace ClassNumberFormula

theorem residue_eq_average_of_coefficients (a : ℕ → ℝ) (ha : ∀ n, 0 ≤ a n) (ρ : ℝ)
    (h : Tendsto (fun N : ℕ => (∑ n ∈ Finset.Icc 1 N, a n) / (N : ℝ)) atTop (𝓝 ρ)) :
    Tendsto (fun s : ℝ => ((s : ℂ) - 1) * LSeries (fun n => (a n : ℂ)) s) (𝓝[>] 1)
      (𝓝 (ρ : ℂ)) := by sorry

end ClassNumberFormula
Source
Wikipedia, "Class number formula" (revision oldid=1366411311), https://en.wikipedia.org/w/index.php?title=Class_number_formula&oldid=1366411311, section "Proof", second paragraph ("An elementary manipulation shows that the residue ... is the average of the coefficients")
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph