# The entropy-rate dimension formula for self-similar measures

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

- [The entropy-rate dimension formula for self-similar measures on the line](../../preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Entropy-rate dimension formula | [SelfSimilar.lean](../ComparatorChallenges/SelfSimilar.lean) |
| Homogeneous-measure and self-similar-attractor dimension formulas | [SelfSimilarCorollaries.lean](../ComparatorChallenges/SelfSimilarCorollaries.lean) |