∑math20

Dynamical systems and ergodic theory · Result 148

The entropy-rate dimension formula for self-similar measures

1 paperLean

For every self-similar measure on the line generated by finitely many contracting similarities, proves \(\dim_{\mathrm H}\mu=\min\{1,h_{\mathrm{RW}}/\chi\}\), where \(h_{\mathrm{RW}}\) is the entropy rate of random composed maps and χ the average logarithmic contraction. This resolves the entropy-rate dimension conjecture without a separation assumption, allowing exact overlaps and unequal contraction ratios.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The entropy-rate dimension formula for self-similar measures on the line

The entropy-rate dimension formula for self-similar measures on the line

OpenAI · September 24, 2026

We prove that the Hausdorff dimension of every finite real self-similar measure equals the minimum of one and its random-walk entropy rate divided by its Lyapunov exponent. Exact overlaps are allowed, and the contraction ratios may be unequal and negative. This resolves the entropy-rate dimension conjecture.

Read PDF Download Source

Cite
@misc{OAI:The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026,
  author = {{OpenAI}},
  title = {{The entropy-rate dimension formula for self-similar measures on the line}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf}{OAI:The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves \(\dim_H\mu=\min\{1,h_{\mathrm{RW}}/\chi\}\) for the lower Hausdorff dimension of every finite real self-similar probability measure with positive weights and nonzero contraction ratios of absolute value below one. Here \(h_{\mathrm{RW}}\) is the entropy rate of random affine compositions and \(\chi\) is the corresponding Lyapunov exponent in the same logarithmic base. Ratios may be signed and unequal, and exact overlaps are allowed.

It also gives two consequences without exact overlaps: the usual entropy-over-Lyapunov formula for a common positive contraction ratio, and the attractor formula \(\dim_H K=\min\{1,s\}\), where \(s\ge0\) is the unique solution of \(\sum_i|r_i|^s=1\). Absolute continuity is outside these statements.

Comparator links

ResultComparator statement
Entropy-rate dimension formulaSelfSimilar.lean
Homogeneous-measure and self-similar-attractor dimension formulasSelfSimilarCorollaries.lean

Scope note on GitHub →