Prove2Me

The Zipf distribution sums to 11

Proved
ZipfLaw.zipfPMF_sum_eq_one

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

harmonic-numberspower-lawzipf-law

For every integer N≥1N\ge1 and real exponent ss,

∑k=1Nf(k;N,s)=∑k=1N1HN,s ks=1.\sum_{k=1}^{N}f(k;N,s)=\sum_{k=1}^N\frac{1}{H_{N,s}\,k^s}=1 .

This is the statement that HN,sH_{N,s} is the normalization constant of the Zipf distribution.

Preamble
import Mathlib
import Definitions.Def_ZipfLaw_Defs
Formal statement
namespace ZipfLaw

theorem zipfPMF_sum_eq_one (N : ℕ) (hN : 1 ≤ N) (s : ℝ) :
    ∑ k ∈ Finset.Icc 1 N, zipfPMF N 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 "Formal definition" (PMF f(k;N,s)=1HN,s1ksf(k;N,s)=\frac{1}{H_{N,s}}\frac{1}{k^s}, HN,sH_{N,s} the normalization constant).
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≥1N\ge1 and every real ss (no sign restriction): ∑k=1NzipfPMF(N,s,k)=1\sum_{k=1}^{N}\mathrm{zipfPMF}(N,s,k)=1, where on this range zipfPMF(N,s,k)=(1/ks)/∑j=1N1/js\mathrm{zipfPMF}(N,s,k)=(1/k^s)/\sum_{j=1}^N 1/j^s.

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