Exponential growth or decay obeys Benford's law in time average

Proved

BenfordLaw.exponential_growth_benford

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

benford-lawequidistributionleading-digits

Let $Q(t) = C e^{rt}$ with $C > 0$ and growth rate $r \neq 0$ (growth if $r>0$ , decay if $r<0$ ). For every digit $d\in\{1,\dots,9\}$ , the fraction of the time interval $[0,T]$ during which $Q$ has leading digit $d$ tends to the Benford probability:

\lim_{T\to\infty}\frac{\lambda\big(\{t\in[0,T] : D_{10}(Q(t)) = d\}\big)}{T} = \log_{10}\!\left(1+\frac1d\right),

where $\lambda$ is Lebesgue measure on $\mathbb R$ .

This is the continuous-time analogue of the sequence results.

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem exponential_growth_benford (C r : ℝ) (hC : 0 < C) (hr : r ≠ 0)
    (d : ℕ) (hd1 : 1 ≤ d) (hd9 : d ≤ 9) :
    Filter.Tendsto
      (fun T : ℝ =>
        (MeasureTheory.volume
          {t : ℝ | t ∈ Set.Icc 0 T ∧ leadingDigit 10 (C * Real.exp (r * t)) = d}).toReal / T)
      Filter.atTop (nhds (benfordProb 10 d)) := by sorry

end BenfordLaw

Source

Wikipedia, "Benford's law" (https://en.wikipedia.org/wiki/Benford%27s_law), snapshot uploaded by the proposer, section "Distributions known to obey Benford's law" ("If a quantity is exponentially increasing or decreasing in time, then the percentage of time that it has each first digit satisfies Benford's law asymptotically").

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 reals $C, r$ with $C>0$ and $r\neq0$ , and every natural $d$ with $1\le d\le 9$ : as the real number $T\to+\infty$ ,

\frac{\lambda\big(\{t\in\mathbb R : 0\le t\le T \text{ and } \lfloor 10^{\{\log_{10}(C e^{rt})\}}\rfloor = d\}\big)}{T} \longrightarrow \log_{10}(1+1/d),

where $\lambda$ is Lebesgue measure, converted from $[0,\infty]$ to $\mathbb R$ (the set is bounded, so the measure is finite). For $T<0$ the set is empty; only large $T$ matter.

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