Prove2Me

Yule–Simon tail: f(k;ρ)∼C/kρ+1f(k;\rho)\sim C/k^{\rho+1}

Proved
ZipfLaw.yuleSimon_tail

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

harmonic-numberspower-lawzipf-law

For every ρ>0\rho>0 there is a constant C>0C>0 such that the Yule–Simon frequencies f(k;ρ)=ρ B(k,ρ+1)f(k;\rho)=\rho\,B(k,\rho+1) satisfy

f(k;ρ)∼Ckρ+1(k→∞),f(k;\rho)\sim\frac{C}{k^{\rho+1}}\qquad(k\to\infty),

i.e. f(k;ρ) kρ+1/C→1f(k;\rho)\,k^{\rho+1}/C\to1.

Preamble
import Mathlib
import Definitions.Def_ZipfLaw_Defs
Formal statement
namespace ZipfLaw

theorem yuleSimon_tail (ρ : ℝ) (hρ : 0 < ρ) :
    ∃ C : ℝ, 0 < C ∧
      Asymptotics.IsEquivalent Filter.atTop (fun k : ℕ => yuleSimonPMF ρ k)
        (fun k : ℕ => C / (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 "Related laws" ("The tail frequencies of the Yule–Simon distribution are approximately f(k;ρ) ≈ [constant]/k^(ρ+1) for any choice of ρ > 0").
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 real ρ>0\rho>0 there exists a real C>0C>0 such that, as k→∞k\to\infty through the naturals, yuleSimonPMF(ρ,k)\mathrm{yuleSimonPMF}(\rho,k) is asymptotically equivalent (Lean IsEquivalent: the difference is little-o of the second function) to C/kρ+1C/k^{\rho+1} (real power). Here yuleSimonPMF(ρ,k)=ρ Γ(k)Γ(ρ+1)/Γ(k+ρ+1)\mathrm{yuleSimonPMF}(\rho,k)=\rho\,\Gamma(k)\Gamma(\rho+1)/\Gamma(k+\rho+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