Hausdorff dimension of planar box-like self-affine sets with rotations
Antti Käenmäki, R. Dániel Prokaj, Károly Simon, Sascha Troscheit
math.DS
Nov 6, 2026 · v1
TL;DR
The paper's dimension results and proofs are formalised in Lean 4 over Mathlib, using only standard axioms, with a public GitHub repository.
Abstract
We study the Hausdorff dimension of proximal planar self-affine sets whose defining maps have diagonal or anti-diagonal linear parts, with both types present. Such systems are irreducible but not strongly irreducible. Under a projective exponential separation condition, we show that the Hausdorff dimension equals the minimum of $2$ and the affinity dimension, thereby extending the dimension formula of Hochman–Rapaport to all proximal irreducible planar systems. When the affinity dimension is at most an explicit threshold determined by the Lyapunov exponents, the formula holds assuming only that there are no exact overlaps. Above the threshold, it holds under the strong open set condition. These dimension formulae are proved by approximation with finite diagonal subsystems. Assuming projective exponential separation, we also determine the pointwise dimensions of the coordinate projections of the equilibrium state. Below the threshold, the projections are not exact-dimensional: the pointwise dimension of each exists almost everywhere and takes exactly two values, each on a set of positive measure. At or above the threshold, both projections are exact-dimensional with dimension one.
Problem
The question is the Hausdorff dimension of proximal planar box-like self-affine sets whose maps have both diagonal and anti-diagonal linear parts. Such systems are irreducible but not strongly irreducible, so they fall outside the existing Hochman–Rapaport and Rapaport results.
Approach
The dimension formula is proved by approximating the system with finite diagonal subsystems, together with thermodynamic formalism and Ledrappier–Young formulae. Three separation hypotheses are used in different regimes: projective exponential separation, no exact overlaps below an explicit Lyapunov threshold, and the strong open set condition above it. The results and proofs were formalised in Lean 4 over Mathlib with AI-model assistance, and the authors checked that the formal statements match the paper.
Results
Under projective exponential separation, the Hausdorff dimension equals min{2, affinity dimension}, which extends the formula to all proximal irreducible planar systems. Below the threshold, the coordinate projections of the equilibrium state are double-dimensional (the pointwise dimension takes exactly two values), while at or above it they are exact-dimensional with dimension one. The Lean development uses no unproved literature hypotheses.
