A scale-invariant first-digit distribution is Benford

Proved

BenfordLaw.benford_of_scale_invariant

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

benford-lawequidistributionleading-digits

Let $X$ be a random variable on a probability space with $X > 0$ almost surely. Suppose the distribution of its first decimal digit does not depend on the unit of measurement, i.e. for every $c > 0$ and every digit $d$ ,

\mathbb P\big(D_{10}(cX) = d\big) = \mathbb P\big(D_{10}(X)=d\big).

Then the first digit follows Benford's law: for $d\in\{1,\dots,9\}$ ,

\mathbb P\big(D_{10}(X) = d\big) = \log_{10}\!\left(1+\frac1d\right).

This turns the informal "units do not matter" argument of the source into a theorem.

Preamble

import Mathlib
import Definitions.Def_BenfordLaw_Defs

Formal statement

namespace BenfordLaw

theorem benford_of_scale_invariant {Ω : Type*} [MeasurableSpace Ω]
    (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P]
    (X : Ω → ℝ) (hXm : Measurable X) (hXpos : ∀ᵐ ω ∂P, 0 < X ω)
    (hinv : ∀ c : ℝ, 0 < c → ∀ d : ℕ,
      P {ω | leadingDigit 10 (c * X ω) = d} = P {ω | leadingDigit 10 (X ω) = d})
    (d : ℕ) (hd1 : 1 ≤ d) (hd9 : d ≤ 9) :
    (P {ω | leadingDigit 10 (X ω) = d}).toReal = 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 "Invariance" ("When the distribution of the first digits of a data set is scale-invariant (independent of the units that the data are expressed in), it is always given by Benford's law", refs. Pinkham 1961, https://doi.org/10.1214/aoms/1177704862).

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.

Let $\Omega$ carry a $\sigma$ -algebra and a probability measure $P$ , and let $X:\Omega\to\mathbb R$ be measurable with $X>0$ $P$ -a.e. Assume: for every real $c>0$ and every natural $d$ (any $d$ , including $0$ and $d \ge 10$ ),

P\{\omega : \lfloor 10^{\{\log_{10}(c X(\omega))\}}\rfloor = d\} = P\{\omega : \lfloor 10^{\{\log_{10} X(\omega)\}}\rfloor = d\}

(equality in $[0,\infty]$ ). Then for every natural $d$ with $1\le d\le 9$ , $P\{\omega : \lfloor 10^{\{\log_{10}X(\omega)\}}\rfloor = d\}$ , as a real number, equals $\log_{10}(1+1/d)$ .

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