Zipf–Mandelbrot law with Hurwitz-zeta normalization is a distribution

Proved

ZipfLaw.zipfMandelbrotPMF_hasSum_one

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

harmonic-numberspower-lawzipf-law

Let $s>1$ and $q\ge0$ . With normalizing constant $C=\zeta(s,q+1)=\sum_{k\ge1}(k+q)^{-s}$ (Hurwitz zeta), the Zipf–Mandelbrot frequencies

f(k;q,s)=\frac{1}{C}\,\frac{1}{(k+q)^s},\qquad k=1,2,3,\dots

form a probability distribution:

\sum_{k=1}^{\infty}f(k;q,s)=1 .

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipfMandelbrotPMF_hasSum_one (q s : ℝ) (hq : 0 ≤ q) (hs : 1 < s) :
    HasSum (fun k : ℕ => zipfMandelbrotPMF q s k) 1 := by sorry

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, section "Related laws" (

f(k;N,q,s)=\frac1C\frac1{(k+q)^s}

; "The constant C is the Hurwitz zeta function evaluated at s").

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 all reals $q\ge0$ and $s>1$ : the family $k\mapsto\mathrm{zipfMandelbrotPMF}(q,s,k)$ , $k\in\mathbb N$ (value $0$ at $k=0$ , and $1/\big(\zeta_{\mathrm{ser}}(s,q+1)(k+q)^s\big)$ for $k\ge1$ , where $\zeta_{\mathrm{ser}}(s,a)=\sum_{n\ge0}(n+a)^{-s}$ as a tsum), is summable with sum exactly $1$ (Lean HasSum, i.e. unconditional convergence).

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