Prove2Me

Entropy of the Zipf distribution

Proved
ZipfLaw.zipfPMF_entropy

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

harmonic-numberspower-lawzipf-law

For N≥1N\ge1 and real ss, the Shannon entropy (in nats) of the Zipf distribution is

−∑k=1Nf(k;N,s)ln⁡f(k;N,s)=sHN,s∑k=1Nln⁡kks+ln⁡HN,s.-\sum_{k=1}^N f(k;N,s)\ln f(k;N,s)=\frac{s}{H_{N,s}}\sum_{k=1}^N\frac{\ln k}{k^s}+\ln H_{N,s}.
Preamble
import Mathlib
import Definitions.Def_ZipfLaw_Defs
Formal statement
namespace ZipfLaw

theorem zipfPMF_entropy (N : ℕ) (hN : 1 ≤ N) (s : ℝ) :
    -(∑ k ∈ Finset.Icc 1 N, zipfPMF N s k * Real.log (zipfPMF N s k)) =
      s / genHarmonic N s * (∑ k ∈ Finset.Icc 1 N, Real.log k / (k : ℝ) ^ s) +
        Real.log (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 (Entropy sHN,s∑k=1Nln⁡kks+ln⁡HN,s\frac{s}{H_{N,s}}\sum_{k=1}^N\frac{\ln k}{k^s}+\ln 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 every natural N≥1N\ge1 and real ss:

−∑k=1NzipfPMF(N,s,k)⋅ln⁡(zipfPMF(N,s,k))=sgenHarmonic(N,s)⋅∑k=1Nln⁡kks+ln⁡(genHarmonic(N,s)),-\sum_{k=1}^N \mathrm{zipfPMF}(N,s,k)\cdot\ln\big(\mathrm{zipfPMF}(N,s,k)\big)=\frac{s}{\mathrm{genHarmonic}(N,s)}\cdot\sum_{k=1}^N\frac{\ln k}{k^s}+\ln\big(\mathrm{genHarmonic}(N,s)\big),

with natural log (Lean's ln⁡\ln, which satisfies ln⁡x=ln⁡∣x∣\ln x = \ln|x| and ln⁡0=0\ln 0 = 0; all arguments here are positive).

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