Rank $1$ is a mode of the Zipf distribution ( $s\ge0$ )

Proved

ZipfLaw.zipfPMF_mode

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

harmonic-numberspower-lawzipf-law

For $N\ge1$ and exponent $s\ge0$ , the element of rank $1$ is a most probable element of the Zipf distribution: for every natural number $k$ ,

f(k;N,s)\le f(1;N,s)=\frac1{H_{N,s}}.

(For $s=0$ the distribution is uniform and every rank is a mode.)

Preamble

import Mathlib
import Definitions.Def_ZipfLaw_Defs

Formal statement

namespace ZipfLaw

theorem zipfPMF_mode (N : ℕ) (hN : 1 ≤ N) (s : ℝ) (hs : 0 ≤ s) (k : ℕ) :
    zipfPMF N s k ≤ zipfPMF N s 1 := by sorry

end ZipfLaw

Source

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

1

; parameters

s\ge0

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$ , real $s\ge0$ and natural $k$ (any $k$ , including $0$ and $k>N$ , where the left side is $0$ ): $\mathrm{zipfPMF}(N,s,k)\le\mathrm{zipfPMF}(N,s,1)$ .

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

Rank 111 is a mode of the Zipf distribution (s≥0s\ge0s≥0)

Rank $1$ is a mode of the Zipf distribution ( $s\ge0$ )