Haar decompression and amenability of Ellis flows
Daniel Max Hoffmann, Krzysztof Krupiński
math.DS
Jul 27, 2026 · v2
math.LO
TL;DR
The authors used Harmonic's Aristotle to mechanically verify selected statements of the paper in Lean 4; no Lean artifact is described.
Abstract
Let $(X,G)$ be a tame flow and let $K$ be an Ellis group of its enveloping semigroup $E(X,G)$. Although $K$ is a compact Hausdorff topological group in its $τ$-topology, the inclusion $K\hookrightarrow E(X,G)$ need not be Borel. We show that normalized Haar measure on $K$ nevertheless determines, via the Riesz–Markov theorem, a canonical regular Borel probability measure $μ_K$ on $E(X,G)$, called its Haar decompression. Haar decompression gives an exact ergodicity description. For an arbitrary flow $(X,G)$, amenability of its Ellis flow is equivalent to hereditary amenability of all finite powers $X^n$. In the tame setting, $(E(X,G),G)$ is amenable if and only if $(X,G)$ is hereditarily amenable. Moreover, for the minimal left ideal $\mathcal{M}$ in $E(X,G)$ containing $K$, $μ_K$ is $G$-invariant if and only if $(\mathcal{M},G)$ is amenable; when this holds, $μ_K$ is the unique ergodic measure on $\mathcal{M}$ and $\mathcal{M}=\overline{K}$. Then, we conclude that the ergodic measures of $E(X,G)$ are precisely the Haar decompressions associated with amenable minimal left ideals. We also prove that every minimal tame amenable flow is uniquely ergodic and that every ergodic invariant measure on a tame flow has minimal support. Consequently, every ergodic measure on a tame ambit arises by evaluating a suitable Haar decompression.
Problem
For tame flows, the inclusion of an Ellis group into the enveloping semigroup need not be Borel. This blocks transferring Haar measure on the group to invariant measures on the flow and its Ellis semigroup.
Approach
Fragmentedness shows that continuous functions restricted to the Ellis group are measurable for the completed Haar measure. The Riesz–Markov theorem then gives a canonical regular Borel probability measure, the Haar decompression. Amenability of Ellis flows is characterized via hereditary amenability of finite powers. Selected statements were machine-checked in Lean 4 using the Aristotle system.
Results
Amenability of the Ellis flow is equivalent to finite-power hereditary amenability, and for tame flows to hereditary amenability. The ergodic measures on E(X,G) are exactly the Haar decompressions of amenable minimal left ideals. Every minimal tame amenable flow is uniquely ergodic, and ergodic measures on tame flows have minimal support.