Zipf extends to infinitely many items iff $s>1$ ; then $H_{N,s}\to\zeta(s)$

Proved

ZipfLaw.zipf_infinite_extension

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

harmonic-numberspower-lawzipf-law

Let $s\ge0$ . Then:

$\displaystyle\sum_{k=1}^\infty\frac{1}{k^s}$ converges if and only if $s>1$ ;
if $s>1$ , then $H_{N,s}\to\zeta(s)$ as $N\to\infty$ , where $\zeta$ is Riemann's zeta function;
if $s\le1$ , then $H_{N,s}\to+\infty$ as $N\to\infty$ .

So the generalized Zipf distribution can be extended to infinitely many items exactly when $s>1$ , and then its normalizing constant is $\zeta(s)$ (the zeta distribution, or Lotka's law). This is the goal theorem of the mission.

Formalization Note. Item 2 is stated in $\mathbb C$ against Mathlib's riemannZeta, which is defined on all of $\mathbb C$ by analytic continuation. Summability is that of $k\mapsto 1/(k+1)^s$ over $k \in \mathbb N$ .

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipf_infinite_extension (s : ℝ) (hs : 0 ≤ s) :
    (Summable (fun k : ℕ => 1 / ((k : ℝ) + 1) ^ s) ↔ 1 < s) ∧
      (1 < s → Filter.Tendsto (fun N : ℕ => ((genHarmonic N s : ℝ) : ℂ)) Filter.atTop
        (nhds (riemannZeta s))) ∧
      (s ≤ 1 → Filter.Tendsto (fun N : ℕ => genHarmonic N s) Filter.atTop Filter.atTop) := by sorry

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, section "Formal definition" ("The generalized Zipf distribution can be extended to infinitely many items (N = ∞) only if the exponent s exceeds 1. In that case, the normalization constant H_{N,s} becomes Riemann's zeta function ... If the exponent s is 1 or less, the normalization constant H_{N,s} diverges as N tends to infinity").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source article and of the intended meaning. It is not a blind audit by an independent reader, and no reviewer should treat it as one. Please compare it against the Lean code yourself.

For every real $s\ge0$ , all three of the following hold:

the family $k\mapsto 1/(k+1)^s$ , $k\in\mathbb N$ (real power), is summable if and only if $s>1$ ;
if $s>1$ , then the complex numbers $\mathrm{genHarmonic}(N,s)=\sum_{k=1}^N 1/k^s$ (real, cast to $\mathbb C$ ) converge as $N\to\infty$ to $\zeta(s)$ , Mathlib's Riemann zeta function evaluated at the complex number $s$ ;
if $s\le1$ , then $\mathrm{genHarmonic}(N,s)\to+\infty$ as $N\to\infty$ (Lean Tendsto … atTop atTop).

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Zipf extends to infinitely many items iff s>1s>1s>1; then HN,s→ζ(s)H_{N,s}\to\zeta(s)HN,s​→ζ(s)

Zipf extends to infinitely many items iff $s>1$ ; then $H_{N,s}\to\zeta(s)$