Zipf's law: generalized harmonic numbers, Zipf / Zipf–Mandelbrot / Yule–Simon laws

Definition

ZipfLaw_Defs

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

harmonic-numberspower-lawzipf-law

Core definitions for the Zipf's-law mission.

Generalized harmonic number. $H_{N,s}=\sum_{k=1}^N k^{-s}$ for $N\in\mathbb N$ and real $s$ ( $H_{0,s}=0$ ).
Zipf distribution. $f(k;N,s)=\dfrac{1}{H_{N,s}}\dfrac{1}{k^s}$ for $1\le k\le N$ , and $f(k;N,s)=0$ for every other natural number $k$ .
Hurwitz zeta (series form). $\zeta(s,a)=\sum_{n\ge0}(n+a)^{-s}$ .
Zipf–Mandelbrot law (infinite ranks). $f(k;q,s)=\dfrac{1}{\zeta(s,q+1)\,(k+q)^s}$ for $k\ge1$ , and $0$ for $k=0$ .
Yule–Simon distribution. $f(k;\rho)=\rho\,\dfrac{\Gamma(k)\,\Gamma(\rho+1)}{\Gamma(k+\rho+1)}=\rho\,B(k,\rho+1)$ .
Leading decimal digit of a natural number $n\ge1$ : $\lfloor n/10^{\lfloor\log_{10}n\rfloor}\rfloor$ .
Random-typing word probability. With $m$ equiprobable letter keys, each typed with probability $q$ , and a space typed with probability $1-mq$ , the probability that the word following a space is exactly $w$ is $q^{|w|}(1-mq)$ .

These are the objects in which every statement of the mission is phrased.

Formalization Note. Powers are real powers (Real.rpow). The Hurwitz series takes the value $0$ when it is not summable (Lean's tsum convention); statements using it assume $s>1$ . The leading digit of $0$ is $0$ .

Definition code

import Mathlib

/-!
# Zipf's law — core definitions

Shared definitions for the Zipf's-law mission (source: Wikipedia, "Zipf's law").
-/

namespace ZipfLaw

/-- The `N`-th generalized harmonic number `H_{N,s} = ∑_{k=1}^{N} 1 / k^s`
(real exponent `s`; `H_{0,s} = 0`). -/
noncomputable def genHarmonic (N : ℕ) (s : ℝ) : ℝ :=
  ∑ k ∈ Finset.Icc 1 N, 1 / (k : ℝ) ^ s

/-- The (generalized) Zipf distribution on `N` elements with exponent `s`: the element of
rank `k ∈ {1, …, N}` has probability `(1 / k^s) / H_{N,s}`; every other `k` gets `0`. -/
noncomputable def zipfPMF (N : ℕ) (s : ℝ) (k : ℕ) : ℝ :=
  if 1 ≤ k ∧ k ≤ N then (1 / (k : ℝ) ^ s) / genHarmonic N s else 0

/-- The Hurwitz zeta function, as its defining series `ζ(s, a) = ∑_{n ≥ 0} 1 / (n + a)^s`
(the value is `0` when the series is not summable). -/
noncomputable def hurwitzZetaSeries (s a : ℝ) : ℝ :=
  ∑' n : ℕ, 1 / ((n : ℝ) + a) ^ s

/-- The Zipf–Mandelbrot law on the ranks `k = 1, 2, 3, …` with shift `q` and exponent `s`:
`f(k; q, s) = (1 / C) · 1 / (k + q)^s` with normalizing constant
`C = ∑_{k ≥ 1} 1 / (k + q)^s = ζ(s, q + 1)` (Hurwitz zeta). Rank `0` gets `0`. -/
noncomputable def zipfMandelbrotPMF (q s : ℝ) (k : ℕ) : ℝ :=
  if 1 ≤ k then 1 / (hurwitzZetaSeries s (q + 1) * ((k : ℝ) + q) ^ s) else 0

/-- The Yule–Simon distribution with parameter `ρ`:
`f(k; ρ) = ρ · B(k, ρ + 1) = ρ · Γ(k) Γ(ρ + 1) / Γ(k + ρ + 1)` for `k = 1, 2, …`. -/
noncomputable def yuleSimonPMF (ρ : ℝ) (k : ℕ) : ℝ :=
  ρ * (Real.Gamma k * Real.Gamma (ρ + 1) / Real.Gamma (k + ρ + 1))

/-- The leading decimal digit of a natural number (`leadingDigit 0 = 0`). -/
def leadingDigit (n : ℕ) : ℕ :=
  n / 10 ^ Nat.log 10 n

/-- Random typing with `m` equiprobable letter keys, each hit with probability `q`, and a
space bar hit with probability `1 - m q`: the probability that the word (maximal block of
letters) following a space is exactly `w`, namely `q^{|w|} (1 - m q)`. -/
noncomputable def monkeyWordProb (m : ℕ) (q : ℝ) (w : List (Fin m)) : ℝ :=
  q ^ w.length * (1 - m * q)

end ZipfLaw

Source

Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, sections "Formal definition", "Related laws", "Statistical explanations" and the infobox.

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.

The file defines, in namespace ZipfLaw:

$\mathrm{genHarmonic}(N,s)=\sum_{k=1}^{N}1/k^s$ for $N\in\mathbb N$ , $s\in\mathbb R$ , with $k^s$ the real power $\mathrm{rpow}$ (for $k\ge1$ this is the usual $e^{s\ln k}$ ). Empty sum ( $N=0$ ) gives $0$ .
$\mathrm{zipfPMF}(N,s,k) = \dfrac{1/k^s}{\mathrm{genHarmonic}(N,s)}$ if $1\le k\le N$ , else $0$ . (Division by $0$ would give $0$ , but for $N \ge 1$ the denominator is positive.)
$\mathrm{hurwitzZetaSeries}(s,a)=\sum_{n=0}^{\infty}1/(n+a)^s$ as a Lean tsum: equal to the series sum if the family is summable, and $0$ otherwise. Real powers of negative bases follow Lean's $\mathrm{rpow}$ convention (not used when $a > 0$ ).
$\mathrm{zipfMandelbrotPMF}(q,s,k)=1/\big(\mathrm{hurwitzZetaSeries}(s,q+1)\cdot(k+q)^s\big)$ if $k\ge1$ , else $0$ (division by $0$ gives $0$ ).
$\mathrm{yuleSimonPMF}(\rho,k)=\rho\cdot\Gamma(k)\Gamma(\rho+1)/\Gamma(k+\rho+1)$ with Lean's real Gamma function (for $k=0$ , $\Gamma(0) = 0$ in Lean, so the value is $0$ ). No restriction on $\rho$ is built in.
$\mathrm{leadingDigit}(n)=n \operatorname{div} 10^{\lfloor\log_{10}n\rfloor}$ with natural-number floor-log ( $\lfloor\log_{10}0\rfloor := 0$ , so $\mathrm{leadingDigit}(0)=0$ ).
$\mathrm{monkeyWordProb}(m,q,w)=q^{\mathrm{length}(w)}\cdot(1-mq)$ for a finite list $w$ of letters from an $m$ -letter alphabet; no constraints on $m$ , $q$ are built in (the value may be negative or exceed $1$ if $q$ is out of range).

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