Zipf's law is the empirical observation that when a set of measured values is sorted in decreasing order, the value of the n-th entry is often approximately inversely proportional to n. Its best-known instance is word frequency in natural language: in the Brown Corpus the most frequent word, "the", accounts for nearly 7% of all word occurrences, the second, "of", for slightly over 3.5%, and so on. The same rank–size relation has been reported for city populations (Auerbach 1913), firm sizes (Axtell 2001), and many other data sets; it is named after the linguist George Kingsley Zipf (1932, 1935, 1949) and remains a central concept of quantitative linguistics (Piantadosi 2014).
In mathematical statistics the law is formalized as the Zipf distribution, a family of discrete probability distributions whose rank–frequency relation is an inverse power law, together with its relatives: the zeta distribution (Lotka's law), the Zipf–Mandelbrot law and the Yule–Simon distribution. Several generative explanations — random typing (Miller 1957, Li 1992) and preferential attachment — produce power laws by provable mechanisms.
Timeline of the results formalized here:
1913–1932 — Auerbach (city sizes), Estoup (1916), Dewey (1923), Condon (1928) and Zipf (1932) observe the inverse rank–frequency relation.
1957 — Miller: a power law emerges in randomly generated texts (doi:10.2307/1419346).
1992 — Li: in random texts with equiprobable letters, word frequency follows Zipf's macro-trend (doi:10.1109/18.165464).
Setting
For a real exponent s and an integer N≥1, the generalized harmonic number is
HN,s=k=1∑Nks1,HN=HN,1.
The Zipf distribution on N elements with exponent s assigns to the element of rank k∈{1,…,N} the probability
f(k;N,s)=HN,s1ks1.
The classical Zipf law is s=1. The source lists the parameter range s≥0, N∈{1,2,3,…}.
The Riemann zeta function is ζ(s)=∑k≥1k−s for s>1. The Hurwitz zeta function is ζ(s,a)=∑n≥0(n+a)−s. The Zipf–Mandelbrot law on ranks k=1,2,… with shift q and exponent s is f(k;q,s)=C1(k+q)s1 with C=ζ(s,q+1). The Yule–Simon distribution with parameter ρ>0 is f(k;ρ)=ρB(k,ρ+1)=ρΓ(k)Γ(ρ+1)/Γ(k+ρ+1), k=1,2,….
Formalization targets
Goal — the infinite-item extension
For s≥0:
k≥1∑ks1<∞⟺s>1;s>1⟹HN,sN→∞ζ(s);s≤1⟹HN,sN→∞∞.
That is, the generalized Zipf distribution extends to infinitely many items exactly when s>1, in which case the normalizing constant becomes Riemann's zeta function.
Milestones
Normalization: ∑k=1Nf(k;N,s)=1.
CDF: ∑k=1nf(k;N,s)=Hn,s/HN,s for n≤N.
Mean: ∑kkf(k;N,s)=HN,s−1/HN,s.
Variance: HN,sHN,s−2−HN,s2HN,s−12.
Entropy: HN,ss∑k=1Nkslnk+lnHN,s.
Mode: rank 1 is a most probable element (for s≥0).
Ratio: f(1;N,s)/f(n;N,s)=ns — "the most common word occurs about n times the n-th most common one" when s=1.
Log–log linearity: lnf(k;N,s)=−slnk−lnHN,s, an affine function of lnk with slope −s.
Zipf–Mandelbrot: with C=ζ(s,q+1) the law is a probability distribution (s>1, q≥0).
Yule–Simon tail: f(k;ρ)∼C/kρ+1 for some constant C>0.
Random typing (Li): word probability is bounded above and below by a power of the rank.
Benford connection: the leading digits of a Zipf (s=1) random rank follow Benford's law as N→∞.
Significance
The goal pins down exactly when "Zipf's law with infinitely many items" makes sense, and identifies the resulting distribution (the zeta distribution) with Riemann's zeta function. The milestones are the infobox facts that statisticians use when fitting Zipf models (CDF, mean, variance, entropy, mode), the log–log diagnostic used to test data against the law, two of the related laws the source lists (Zipf–Mandelbrot, Yule–Simon), one of the generative explanations (random typing), and the stated link to Benford's law.
The results are classical; the work is formalizing them. Most milestones are finite algebra about HN,s; the goal, the Yule–Simon tail, the random-typing bound and the Benford connection need analysis.
Difficulty
The finite identities are routine once the support conventions are fixed. The analytic content is concentrated in four places. The goal needs the p-series test and the identification of the limit with Mathlib's complex riemannZeta, which is defined by analytic continuation rather than by the series. The Yule–Simon tail needs the asymptotics Γ(k)/Γ(k+a)∼k−a. The random-typing bound requires controlling the rank of a word through the number of strictly shorter words, uniformly over every rank order compatible with the probabilities. The Benford connection requires comparing the harmonic sums over each block of integers with a fixed leading digit with ln(1+1/d), with an error that is negligible against HN∼lnN.
Formalization scope
HN,s uses a real exponent (Real.rpow); H0,s=0.
zipfPMF N s k is defined for every natural k and is 0 outside the support {1,…,N}. Statements that need a nonempty support assume N≥1.
The goal states convergence to the complex number riemannZeta s of the real partial sums viewed as complex numbers, and divergence as Tendsto … atTop atTop. The source's parameter range s≥0 is kept as a hypothesis.
The Hurwitz zeta function is defined by its series (value 0 when the series diverges); the Zipf–Mandelbrot law is the infinite-item version on ranks k≥1, with q≥0.
The Yule–Simon distribution is defined through the Gamma function; the tail statement asserts existence of a positive constant, matching the source's "[constant]".
Random typing is formalized in Li's equiprobable model: m≥2 letters each typed with probability q>0, a space with probability 1−mq>0, and a word w has probability q∣w∣(1−mq). "Sorted by rank" means any bijection e from N onto the nonempty words along which the probability is non-increasing; the conclusion is a two-sided power-law bound with exponent logm(1/q).
The Benford connection uses the leading decimal digit of the rank k, with k drawn from the Zipf distribution with s=1.
Not formalized: the empirical claims (word, city, income data), the atlas-model result, Belevitch's Taylor-series argument, the parabolic fractal distribution and the Pareto exchange of variables; their statements in the source are not precise enough to formalize faithfully.
G. A. Miller, Some effects of intermittent silence, American Journal of Psychology 70 (1957), 311–314. https://doi.org/10.2307/1419346
W. Li, Random texts exhibit Zipf's-law-like word frequency distribution, IEEE Trans. Inform. Theory 38 (1992), 1842–1845. https://doi.org/10.1109/18.165464
B. Conrad, M. Mitzenmacher, Power laws for monkeys typing randomly: the case of unequal probabilities, IEEE Trans. Inform. Theory 50 (2004), 1403–1414. https://doi.org/10.1109/TIT.2004.830752
S. T. Piantadosi, Zipf's word frequency law in natural language: a critical review and future directions, Psychon. Bull. Rev. 21 (2014), 1112–1130. https://doi.org/10.3758/s13423-014-0585-6
Goal · Zipf extends to infinitely many items iff s>1; then HN,s→ζ(s)
PROVED
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
Let s≥0. Then:
k=1∑∞ks1 converges if and only if s>1;
if s>1, then HN,s→ζ(s) as N→∞, where ζ is Riemann's zeta function;
if s≤1, then HN,s→+∞ as N→∞.
So the generalized Zipf distribution can be extended to infinitely many items exactly when s>1, and then its normalizing constant is ζ(s) (the zeta distribution, or Lotka's law). This is the goal theorem of the mission.
Formalization Note. Item 2 is stated in C against Mathlib's riemannZeta, which is defined on all of C by analytic continuation. Summability is that of k↦1/(k+1)s over k∈N.
Frontier · Open leaf nodes
Recent activity
Frontier · Open leaf nodes
No open leaves. Every sub-goal is proved or awaiting decomposition.