Prove2Me

CDF of the Zipf distribution: Hn,s/HN,sH_{n,s}/H_{N,s}

Proved
ZipfLaw.zipfPMF_cdf

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

harmonic-numberspower-lawzipf-law

For integers N≥1N\ge1, 0≤n≤N0\le n\le N and real ss, the cumulative distribution function of the Zipf distribution is

∑k=1nf(k;N,s)=Hn,sHN,s.\sum_{k=1}^{n}f(k;N,s)=\frac{H_{n,s}}{H_{N,s}} .
Preamble
import Mathlib
import Definitions.Def_ZipfLaw_Defs
Formal statement
namespace ZipfLaw

theorem zipfPMF_cdf (N : ℕ) (hN : 1 ≤ N) (s : ℝ) (n : ℕ) (hn : n ≤ N) :
    ∑ k ∈ Finset.Icc 1 n, zipfPMF N s k = genHarmonic n s / genHarmonic N s := by sorry

end ZipfLaw
Source
Wikipedia, "Zipf's law" (https://en.wikipedia.org/wiki/Zipf%27s_law), snapshot uploaded by the proposer, infobox (CDF Hk,s/HN,sH_{k,s}/H_{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 all naturals N≥1N\ge1 and n≤Nn\le N and every real ss: ∑k=1nzipfPMF(N,s,k)=genHarmonic(n,s)/genHarmonic(N,s)\sum_{k=1}^{n}\mathrm{zipfPMF}(N,s,k)=\mathrm{genHarmonic}(n,s)/\mathrm{genHarmonic}(N,s). For n=0n=0 both sides are 00.

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