Lean Formalisation

Lean Formalisation

This page is an inventory of the results I have (auto-)formalised in Lean 4 with Mathlib, with links to the respective Github project and Palomar record, if available.

Quick links:

My papers

Lecture notes

  • Sascha Troscheit. Geometric Measure Theory: Dynamics and Randomness. Lecture notes, Uppsala University, (2026), PDF.
    GitHub: sascha2718/lean-geometric-measure-theory.
    • Every numbered result of Sections 1 to 8 except Theorem 5.11 is formalised. Theorem 3.19 is formalised for 0 < s < 1 and Theorem 3.28 assumes the Besicovitch density bound.

Results from the literature

  • Balázs Bárány, Antti Käenmäki, and Han Yu. Finer geometry of planar self-affine sets. Advances in Mathematics, 493, 110914, (2026).
    GitHub: sascha2718/lean-fractal-geometry.
    • Lemma 2.7.
  • Rufus Bowen. Equilibrium states and the ergodic theory of Anosov diffeomorphisms. Lecture Notes in Mathematics, 470, Springer, (1975).
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 1.4, for a mixing parity shift.
  • Leo Breiman. The individual ergodic theorem of information theory. Annals of Mathematical Statistics, 28(3), (1957), 809–811.
    GitHub: sascha2718/lean-fractal-geometry.
    • The Shannon–McMillan–Breiman theorem, for two-sided shifts over a finite alphabet.
  • Manfred Einsiedler and Thomas Ward. Ergodic Theory with a View Towards Number Theory. Graduate Texts in Mathematics, 259, Springer, (2011).
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2.30, the pointwise ergodic theorem.
    • Theorem 5.14 and Proposition 5.20.
  • Kenneth J. Falconer. The Hausdorff dimension of self-affine fractals. Mathematical Proceedings of the Cambridge Philosophical Society, 103(2), (1988), 339–350.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 5.4, the upper bound, in the plane.
  • William Feller. An Introduction to Probability Theory and Its Applications, Volume II. Second edition, John Wiley & Sons, (1971).
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2 of Section XI.1, the key renewal theorem, and its form (9.2) on the whole line in Section XI.9, for finite self-similar laws.
  • De-Jun Feng. Dimension of invariant measures for affine iterated function systems. Duke Mathematical Journal, 172(4), (2023), 701–774.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorems 1.2(ii) and 1.3, in the plane.
  • De-Jun Feng and Huyi Hu. Dimension theory of iterated function systems. Communications on Pure and Applied Mathematics, 62(11), (2009), 1435–1500.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2.8, for self-similar systems on the line.
  • De-Jun Feng and Antti Käenmäki. Equilibrium states of the pressure function for products of matrices. Discrete and Continuous Dynamical Systems, 30(3), (2011), 699–708.
    GitHub: sascha2718/lean-fractal-geometry.
    • Proposition 1.2, in the plane.
  • Jonathan M. Fraser. On the packing dimension of box-like self-affine sets in the plane. Nonlinearity, 25(7), (2012), 2075–2092.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2.3 and Corollary 2.5.
  • Jonathan M. Fraser, Thomas Jordan, and Natalia Jurga. Dimensions of equilibrium measures on a class of planar self-affine sets. Journal of Fractal Geometry, 7(1), (2020), 87–111.
    GitHub: sascha2718/lean-fractal-geometry.
    • Lemma 1.3 and Corollaries 1.5 and 1.6, the decomposition and Lyapunov exponent parts.
  • Harry Furstenberg and Harry Kesten. Products of random matrices. Annals of Mathematical Statistics, 31(2), (1960), 457–469.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2, for planar matrices.
  • Dimitrios Gatzouras and Steven P. Lalley. Statistically self-affine sets: Hausdorff and box dimensions. Journal of Theoretical Probability, 7(2), (1994), 437–468.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 4.1 and Proposition 3.5, for independent Bernoulli retention.
  • John E. Hutchinson. Fractals and self-similarity. Indiana University Mathematics Journal, 30(5), (1981), 713–747.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorems 3.1(3), 4.4(1) and 5.3(1), for systems on the line.
  • Thomas Jordan and Ariel Rapaport. Dimension of ergodic measures projected onto self-similar sets with overlaps. Proceedings of the London Mathematical Society, 122(2), (2021), 191–206.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 1.1.
  • Shuo-Yen Robert Li. A martingale approach to the study of occurrence of sequence patterns in repeated experiments. Annals of Probability, 8(6), (1980), 1171–1176.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 3.1, for patterns of equal length.
  • Russell Lyons and Yuval Peres. Probability on Trees and Networks. Cambridge Series in Statistical and Probabilistic Mathematics, 42, Cambridge University Press, (2016).
    GitHub: sascha2718/lean-branching-processes and sascha2718/lean-fractal-geometry.
    • Proposition 5.28, the decomposition of a supercritical tree, for bounded offspring support.
  • John M. Mackay. Assouad dimension of self-affine carpets. Conformal Geometry and Dynamics, 15, (2011), 177–187.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 1.1.
  • Ian D. Morris and Pablo Shmerkin. On equality of Hausdorff and affinity dimensions, via self-affine measures on positive subsystems. Transactions of the American Mathematical Society, 371(3), (2019), 1547–1582.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 3.1 and Lemmas 3.4 and 3.5, for rectangular systems.
  • V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov exponents of dynamical systems. Trudy Moskovskogo Matematicheskogo Obshchestva, 19, (1968), 179–210.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 1 of Section 3, for planar matrices with distinct Lyapunov exponents.
  • Andreas Schief. Separation properties for self-similar sets. Proceedings of the American Mathematical Society, 122(1), (1994), 111–115.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 2.1, for systems on the line.
  • Pablo Shmerkin. On Furstenberg’s intersection conjecture, self-similar measures, and the L^q norms of convolutions. Annals of Mathematics, 189(2), (2019), 319–391.
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 6.6, the lower bound.
    • Theorem 3.1, in a weaker form.
  • J. Michael Steele. Kingman’s subadditive ergodic theorem. Annales de l’Institut Henri Poincaré, Probabilités et Statistiques, 25(1), (1989), 93–98.
    GitHub: sascha2718/lean-fractal-geometry.
    • The theorem of Section 1, Kingman’s subadditive ergodic theorem.
  • Peter Walters. An Introduction to Ergodic Theory. Graduate Texts in Mathematics, 79, Springer, (1982).
    GitHub: sascha2718/lean-fractal-geometry.
    • Theorem 4.17, the Kolmogorov–Sinai theorem, for two-sided shifts over a finite alphabet.

The fractal geometry library also contains Theorem 1.1 of Samuel Kittle and Constantin Kogler, The exact overlaps conjecture for self-similar measures on the real line, preprint (2026), taken from the authors’ formalisation.

Libraries