Papers With

← All papers
First page of The Exact Overlaps Conjecture for Self-Similar Measures on the Real Line

The Exact Overlaps Conjecture for Self-Similar Measures on the Real Line

Samuel Kittle, Constantin Kogler

math.DS Oct 7, 2026 · v1 math.PR
formalization probability
Read PDF arXiv abstract Code
TL;DR
All results, plus needed prior results such as Hochman's Theorem 1.4, were formalized in Lean, with source code in an accompanying repository.
Abstract
A generalization of the exact overlaps conjecture predicts a formula for the dimension of self-similar measures in terms of the random walk entropy and the Lyapunov exponent. We prove the exact overlaps conjecture and its generalized version in dimension one. The proof relies on a new entropy inequality quantifying the information lost under addition of independent random variables in terms of a quantity averaging variance across scales.
Problem

The generalized exact overlaps conjecture predicts that the dimension of a self-similar measure on the real line equals min{1, h_mu/|chi_mu|}, given by the random walk entropy and the Lyapunov exponent. Hochman settled it under exponential separation, but transcendental parameters remained open.

Approach

The authors prove a new entropy inequality bounding the information lost when adding independent random variables by a quantity that averages variance across scales. The proof reveals the summands gradually through Poisson-process interval partitions and uses Margulis-Russo-type derivative formulas. Combined with Hochman's inverse theorem and a multiscale argument on stopped random walks, this yields the dimension formula. The results and the required prior results were formalized in Lean.

Results

The exact overlaps conjecture and its generalized version are proved in dimension one. A Lean formalization of all results is publicly available.