Variance of the Zipf distribution

Proved

ZipfLaw.zipfPMF_variance

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

harmonic-numberspower-lawzipf-law

For $N\ge1$ and real $s$ , the variance of the rank under the Zipf distribution is

\sum_{k=1}^N k^2 f(k;N,s)-\Big(\sum_{k=1}^N k\,f(k;N,s)\Big)^2=\frac{H_{N,s-2}}{H_{N,s}}-\frac{H_{N,s-1}^2}{H_{N,s}^2}.

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipfPMF_variance (N : ℕ) (hN : 1 ≤ N) (s : ℝ) :
    (∑ k ∈ Finset.Icc 1 N, (k : ℝ) ^ 2 * zipfPMF N s k) -
        (∑ k ∈ Finset.Icc 1 N, (k : ℝ) * zipfPMF N s k) ^ 2 =
      genHarmonic N (s - 2) / genHarmonic N s -
        genHarmonic N (s - 1) ^ 2 / genHarmonic N s ^ 2 := by sorry

end ZipfLaw

Source

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

\frac{H_{N,s-2}}{H_{N,s}}-\frac{H^2_{N,s-1}}{H^2_{N,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 every natural $N\ge1$ and real $s$ :

\Big(\sum_{k=1}^N k^2\,\mathrm{zipfPMF}(N,s,k)\Big)-\Big(\sum_{k=1}^N k\,\mathrm{zipfPMF}(N,s,k)\Big)^2=\frac{\mathrm{genHarmonic}(N,s-2)}{\mathrm{genHarmonic}(N,s)}-\frac{\mathrm{genHarmonic}(N,s-1)^2}{\mathrm{genHarmonic}(N,s)^2},

with $k^2$ a natural-exponent power of the real $k$ .

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