14 Pesin’s entropy formula (volume case)
The Margulis–Ruelle inequality of Chapter 10 bounds the Kolmogorov–Sinai entropy of a smooth ergodic map from above by its positive Lyapunov exponents, \(h_\mu (T)\le \sum _{\lambda _i{\gt}0}\lambda _i\). Pesin’s theorem asserts that for the geometrically distinguished SRB (Sinai–Ruelle–Bowen) measures this bound is an equality,
identifying metric entropy with the total exponential stretching along unstable directions. This chapter formalizes the reverse inequality \(\sum _{\lambda _i{\gt}0}\lambda _i\le h_\mu (T)\) and the resulting equality in the volume case — the honest fragment of the SRB condition that is expressible without the Pesin unstable-manifold / foliation machinery Mathlib lacks — and closes with the first non-vacuous full-system witness, the doubling map on the circle (\(h_\mu (T)=\sum \lambda ^{+}=\log 2\)). This is the second hard leaf of the smooth theory (issue #10); the general mixed-spectrum Ledrappier–Young reverse inequality remains a disclosed Mathlib-scale wall.
The upper bound is the sharp Margulis–Ruelle inequality Theorem 10.23, which needs no SRB hypothesis and is developed in the classical-entropy chapter; here we recall it only as the \(\le \) direction and concentrate on the reverse. The reverse inequality does not go through the general Ledrappier–Strelcyn–Young route (absolute continuity of the conditional measures on unstable manifolds, unavailable in Mathlib); instead it is discharged, in the volume case, from Rokhlin’s inequality — an unconditional, generator-free lower bound \(\int \log \left\lvert \det D_xT \right\rvert \, d\mu \le h_\mu (T)\) — together with the trace–determinant identity and a nonnegative-spectrum gate. Throughout, the phase space is \(E=\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\), \(\mu \) is a probability measure, \(T\) is differentiable with everywhere-nonsingular derivative, and the derivative cocycle \(x\mapsto D_xT\) (Definition 13.1) carries log-integrable data (Definition 2.4 for \(DT\) and \(DT^{-1}\)), so that the multiplicative ergodic theorem supplies the Lyapunov exponents \(\lambda _i\) (Definition 6.11).
14.1 Rokhlin’s inequality: the generator-free lower bound
Rokhlin’s volume-distortion identity \(h_\mu (T,\xi )=\int \log \left\lvert \det D_xT \right\rvert \, d\mu \) (Theorem 10.24) needs a one-sided generating cell-injective partition. Dropping the generating hypothesis while keeping the injectivity change-of-variables computation (Theorem 13.11) turns the identity into a one-sided, partition-free inequality, which is exactly the reverse half of Pesin’s theorem in the absolutely continuous case. The key structural fact making this unconditional is that the strict-future \(\sigma \)-algebra of any partition sits below the comap of \(T\).
For a measure-preserving \(T\) and a finite measurable partition \(\xi \), the strict-future \(\sigma \)-algebra generated by the pullbacks of the iterated joins lies below the comap of \(T\):
This is the generator-free half of the equality \(\bigvee _k\sigma (\dots )=\operatorname {comap}T\, m_E\) that holds for a one-sided generating partition: the reverse containment needs generation, but \(\le \) is unconditional. Per term the pulled-back generated \(\sigma \)-algebra equals the comap of \(T\) applied to the join’s own generated \(\sigma \)-algebra, which is below \(m_E\); iSup_le and monotonicity of comap close the bound. This \(\le \) is precisely what removes the generator hypothesis from Rokhlin’s inequality below.
Let \(T\) be a measure-preserving, differentiable self-map of \(\mathbb {R}^d\) with \(\mu \ll \operatorname {volume}\) and everywhere-nonsingular derivative, let \(\xi \) be a nonempty injectivity partition (Definition 13.10), and assume \(\log \rho \in L^1(\mu )\) for the density \(\rho =d\mu /d\operatorname {vol}\) and \(\log \left\lvert \det DT \right\rvert \in L^1(\mu )\). Then, with no generating-partition hypothesis,
This is the generator-free lower bound on entropy (Rokhlin 1967, §9; Parry 1969; Coudène, Ergodic Theory and Dynamical Systems, Cor. 12.1): the integrated log volume distortion never exceeds the Kolmogorov–Sinai entropy. It needs no ergodicity and no expansion — those enter only for Rokhlin’s equality. Here \(\mu \ll \operatorname {volume}\) enters solely through Coudène’s Remark \(\left\lvert T'_\mu \right\rvert =\left\lvert \det DT \right\rvert \) a.e., identifying the Radon–Nikodym distortion with the Jacobian determinant. The hypotheses are non-vacuous on \(\mathbb {R}^d\): e.g. \(T=\operatorname {id}\) with any a.c. probability \(\mu \) gives \(0\le h_\mu (\operatorname {id})\).
Four steps chain. First, the injectivity change-of-variables computation (Theorem 13.11) evaluates the conditional entropy of \(\xi \) against \(\operatorname {comap}T\, m_E\) to \(\int \log \left\lvert \det D_xT \right\rvert \, d\mu \), independently of the partition. Second, conditioning is antitone in the \(\sigma \)-algebra, so Lemma 14.1 bounds \(H(\xi \mid \operatorname {comap}T\, m_E)\) above by \(H(\xi \mid \mathcal S_\infty )\) against the larger strict-future \(\sigma \)-algebra \(\mathcal S_\infty \). Third, the sharp-rate identity (Theorem 11.4) identifies \(H(\xi \mid \mathcal S_\infty )\) with the per-partition entropy \(h_\mu (T,\xi )\). Finally \(h_\mu (T,\xi )\le h_\mu (T)\) lifts to the system entropy, and the fixed left-hand side survives all three monotone steps.
14.2 The SRB property and the unstable-Jacobian bridge
Pesin’s formula holds exactly for SRB measures: those whose conditional measures on unstable manifolds are absolutely continuous with respect to leaf (Riemannian) volume (Ledrappier–Strelcyn–Young). In full generality that condition is not stateable in Mathlib — it needs the Pesin unstable-manifold theorem integrating the measurable distribution \(E^u\) into the foliation \(W^u\), the disintegration of \(\mu \) along that specific foliation, and the leaf-volume measure, none of which exist in the library. What is expressible is the volume case: the situation in which the whole space is a single unstable leaf, so leaf volume is ambient volume and the SRB condition collapses to \(\mu \ll \operatorname {volume}\).
A map \(T\) preserves an SRB (volume-case) measure \(\mu \) if \(\mu \) is absolutely continuous with respect to ambient Lebesgue volume, \(\mu \ll \operatorname {volume}\). This is the volume-case specialization of the Ledrappier–Strelcyn–Young SRB condition. It is a genuine, non-vacuous, dischargeable hypothesis: \(\operatorname {volume}\ll \operatorname {volume}\) witnesses inhabitation, while a Dirac mass is not \(\ll \operatorname {volume}\). Three earlier framings on issue #10 were all defective and are recorded so the rescope is auditable: an \(\texttt{acConditionalUnstable}:\texttt{True}\) field (vacuous, dischargeable by \(\langle \texttt{trivial}\rangle \)); an existential \(\exists \pi \, \eta ,\ \operatorname {singularPart}(\operatorname {condDistrib}\dots )=0\) (also vacuous — satisfied by every \(\mu \), since an existential over an arbitrary measurable factor self-trivializes); and an \(\texttt{opaque}\) marker (honest but unconsumable, so the reverse inequality stayed a documented \(\texttt{BLOCKED}\) leaf). The field \(\mu \ll \operatorname {volume}\) is the honest fix that is both genuine and consumable — the reverse inequality is proved from it.
For an ergodic differentiable \(T\) with nonsingular log-integrable derivative cocycle, the predicate \(\operatorname {UnstableJacobianRate}\, \chi \) asserts that a candidate integrand \(\chi :E\to \mathbb {R}\) is \(\mu \)-a.e. equal to the deterministic positive-exponent sum \(\sum _i\lambda _i^{+}=\operatorname {sumPosExp}\). Geometrically \(\chi (x)\) is meant to be the a.e. orbit growth rate of the unstable Jacobian \(\log \left\lvert \det (D_xT^{[n]})|_{E^u(x)} \right\rvert \); since the spectrum is a.e. constant by ergodicity, that rate is a.e. the constant \(\operatorname {sumPosExp}\). This is the bridge object that phrases Pesin’s formula in its genuine integral form \(h_\mu (T)=\int \chi \, d\mu \): a probability measure integrates the a.e.-constant \(\chi \) to itself, \(\int \chi \, d\mu =\operatorname {sumPosExp}\). In the volume case the reverse inequality is proved without this interface (it goes through Rokhlin’s inequality directly); the object is retained only to state the literal integral form.
14.3 The reverse inequality and the spectrum gate
The reverse inequality chains Rokhlin’s inequality with the trace–determinant identity, gated by a nonnegative Lyapunov spectrum. The gate is exactly where the volume case is delimited.
If every Lyapunov exponent of the derivative cocycle is nonnegative, \(0\le \lambda _i\) for all \(i\), then the positive-part exponent sum equals the full exponent sum, \(\sum _i\lambda _i^{+}=\sum _i\lambda _i\).
The two finite sums differ only in the summands with \(\lambda _i\le 0\); under the hypothesis those are \(\lambda _i=0\), which contribute nothing to either side.
Let \(T\) be ergodic on \(\mathbb {R}^d\) with a nonsingular, log-integrable derivative cocycle, differentiable, preserving an SRB (volume-case) measure (\(\mu \ll \operatorname {volume}\), Definition 14.3), equipped with a nonempty injectivity partition \(\xi \) and integrable \(\log \rho ,\ \log \left\lvert \det DT \right\rvert \). If the Lyapunov spectrum is nonnegative (\(0\le \lambda _i\) for all \(i\), the hypothesis hspec), then
the reverse of the sharp Margulis–Ruelle bound (Pesin 1977; Mañé 1981; Ledrappier–Young 1985), discharged here via Rokhlin’s inequality.
The chain is \(\sum \lambda ^{+}\overset {(1)}{=}\sum \lambda \overset {(2)}{=}\int \log \left\lvert \det D_xT \right\rvert \, d\mu \overset {(3)}{\le }h_\mu (T)\). Step (1) is Lemma 14.5: the nonnegative spectrum kills the negative part. Step (2) is the trace–determinant identity (Theorem 6.20) aligned to the Fréchet-derivative determinant. Step (3) is Rokhlin’s inequality (Theorem 14.2).
The spectrum gate hspec is exactly the volume-case boundary and is not derivable from \(\mu \ll \operatorname {volume}\). In the volume regime there are no genuinely negative exponents, so \(\int \log \left\lvert \det DT \right\rvert \, d\mu =\sum \lambda ^{+}\) and the chain closes. For a mixed-spectrum SRB measure with real stable directions, \(\int \log \left\lvert \det DT \right\rvert \, d\mu =\sum \lambda ^{+}+\sum \lambda ^{-}{\lt}\sum \lambda ^{+}\), so Rokhlin’s inequality yields only the weaker \(\sum \lambda ^{+}+\sum \lambda ^{-}\le h_\mu (T)\); recovering the full reverse inequality then requires the Ledrappier–Young unstable-Jacobian machinery — the documented Mathlib-scale wall. (Volume-preserving hyperbolic maps have \(\int \log \left\lvert \det \right\rvert =0\) with genuinely negative exponents, so hspec is a real, separate hypothesis, not a consequence of absolute continuity.)
14.4 Pesin’s entropy formula
Combining the sharp Margulis–Ruelle upper bound with the volume-case reverse leaf by antisymmetry gives Pesin’s formula in the volume case, in both a clean spectral form and the genuine integral form.
For an ergodic differentiable self-map \(T\) of \(\mathbb {R}^d\) preserving an SRB (volume-case) measure \(\mu \) (Definition 14.3) with nonsingular log-integrable derivative cocycle and nonnegative Lyapunov spectrum (hspec), and under the honest non-compactness atom-count input hgeo of the sharp Margulis–Ruelle inequality, the Kolmogorov–Sinai entropy equals the sum of the strictly positive Lyapunov exponents:
This is Pesin’s entropy formula in the absolutely continuous case (Pesin 1977; Ledrappier–Young 1985), obtained here foliation-free.
Antisymmetry of the two inequalities. The \(\le \) direction \(h_\mu (T)\le \sum \lambda ^{+}\) is the sharp Margulis–Ruelle inequality (Theorem 10.23), which holds for every invariant measure — no SRB hypothesis — and carries only its atom-count input hgeo. The \(\ge \) direction \(\sum \lambda ^{+}\le h_\mu (T)\) is the volume-case reverse leaf (Theorem 14.6). The hypotheses of the formula are exactly the union of the two halves.
Under the same hypotheses, with \(\chi \) an unstable-Jacobian integrand (Definition 14.4), the system entropy is the literal Pesin integral
The bridge \(\int \chi \, d\mu =\operatorname {sumPosExp}\) holds because \(\chi \) is \(\mu \)-a.e. equal to the constant \(\operatorname {sumPosExp}\) (Definition 14.4) and \(\mu \) is a probability measure, so \(\int \chi \, d\mu =\operatorname {sumPosExp}\cdot \mu (E)=\operatorname {sumPosExp}\) via integral_congr_ae; no integrability hypothesis on \(\chi \) is needed. Rewriting through this bridge reduces the claim to the spectral form (Theorem 14.7).
Vacuity disclosure (honest).
Exactly as for the expanding-map assembly Theorem 13.12, these EuclideanSpace theorems are correct implications whose joint hypothesis bundle has no known model on the non-compact space \(\mathbb {R}^d\). The bundle asks for an ergodic, absolutely continuous probability measure preserved by an everywhere-nonsingular map with no negative exponents (hspec); on \(\mathbb {R}^d\) these clash — an all-nonnegative spectrum expands volume on average, which on a non-compact space forces mass to escape to infinity, incompatible with an a.c. invariant probability. So on \(\mathbb {R}^d\) the statements are (as far as is known) vacuously-true assemblies of the implication, not exhibited instances. The genuinely witnessed equality lives on the compact circle, developed next.
14.5 A witnessed instance: the doubling map
The vacuity of the \(\mathbb {R}^d\) bundle is escaped on a compact carrier. For the doubling map \(T:y\mapsto 2\cdot y\) on the unit circle \(\mathbb T=\operatorname {UnitAddCircle}\) (), ergodic for Haar measure (), the binary partition \(\alpha =\{ [0,\tfrac 12),[\tfrac 12,1)\} \) () is a genuine one-sided generator, so both sides of Pesin’s formula are computed and equal \(\log 2\). This is the first non-vacuous full-system instance of the volume-case formula in the library — positive entropy on a compact space, every input honest.
For the doubling map and its binary partition, the partition-relative Kolmogorov–Sinai entropy equals the sum of the positive Lyapunov exponents, both being \(\log 2\): \(h_\mu (T,\alpha )=\sum \lambda ^{+}\).
The entropy side is \(h_\mu (T,\alpha )=\log 2\) (Theorem 13.17), the exponent side is \(\sum \lambda ^{+}=\log 2\) (Corollary 13.14); the two agree.
The generator crux: dyadic arcs generate the Borel structure
Upgrading the per-partition identity to the full system \(h_\mu (T)=h_\mu (T,\alpha )\) requires the binary partition to generate: its forward \(T\)-translates must recover every Borel set. This reduces to showing the countable family of dyadic arcs generates the Borel \(\sigma \)-algebra, proved by a binary-expansion measurability argument.
The set of all \(n\)-fold-join cells of the binary partition under the doubling map, \(\bigcap _{k{\lt}n}T^{-k}\bigl(\operatorname {binCell}(f(k))\bigr)\) over all lengths \(n\) and digit strings \(f:\operatorname {Fin}n\to \operatorname {Fin}2\). Each such set is a dyadic arc of length \(2^{-n}\).
The \(n\)-th binary digit \(d_n(y)=\mathbf1_{T^{-n}(\operatorname {binCell}1)}(y)\in \{ 0,1\} \) records whether \(T^n y\) lands in the right half; the \(N\)-th dyadic partial sum
() is the truncated binary expansion of the canonical representative \(\operatorname {rep}(y)\in [0,1)\) ().
On the representative, the doubling map acts by \(x\mapsto 2x\) on the left half and \(x\mapsto 2x-1\) on the right, uniformly \(\operatorname {rep}(Ty)=2\operatorname {rep}(y)-d_0(y)\).
Case split on \(y\in \operatorname {binCell}1\). On the right half \(d_0=1\) and \(2\operatorname {rep}(y)-1\in [0,1)\), which is the representative of \(2y\) after subtracting the integer \(1\) killed by the projection \(\mathbb {R}\to \mathbb T\); on the left half \(d_0=0\) and \(2\operatorname {rep}(y)\in [0,1)\) is already the representative.
The representative splits into its first \(N\) digits plus a rescaled tail: \(\operatorname {rep}(y)=\operatorname {binPartialSum}N(y)+\operatorname {rep}(T^N y)\, 2^{-N}\).
Induction on \(N\), feeding the one-step recursion Lemma 14.12 into the tail (using that the \(0\)-th digit at \(T^N y\) is the \(N\)-th digit at \(y\)).
\(\operatorname {binPartialSum}N(y)\to \operatorname {rep}(y)\) as \(N\to \infty \).
The tail remainder \(\operatorname {rep}(T^N y)\, 2^{-N}\le 2^{-N}\to 0\) is squeezed to zero, so the partial sums converge to \(\operatorname {rep}(y)\) by Lemma 14.13.
Each digit set \(T^{-n}(\operatorname {binCell}1)\) is the finite union of the generation-\((n+1)\) dyadic arcs whose last digit is \(1\), hence \(\operatorname {generateFrom}(\operatorname {dyadicArcSet})\)-measurable.
A point lies in \(T^{-n}(\operatorname {binCell}1)\) iff its length-\((n+1)\) digit string has last digit \(1\); realizing the string as the join cell exhibits the digit set as a finite union of arcs from Definition 14.10.
\(\operatorname {rep}\) is \(\operatorname {generateFrom}(\operatorname {dyadicArcSet})\)-measurable.
Each digit function is the indicator of a dyadic-measurable digit set (Lemma 14.15), so each finite partial sum is dyadic-measurable; the pointwise limit \(\operatorname {rep}\) (Lemma 14.14) inherits measurability by measurable_of_tendsto_metrizable’.
The Borel \(\sigma \)-algebra of the circle lies below the one generated by the dyadic arcs, \(m_{\mathbb T}\le \operatorname {generateFrom}(\operatorname {dyadicArcSet})\).
Since \((\uparrow )\circ \operatorname {rep}=\operatorname {id}\) factors the identity through the measurable covering projection \(\mathbb {R}\to \mathbb T\), the Borel structure pulls back through \(\operatorname {rep}\) into \(\operatorname {generateFrom}(\operatorname {dyadicArcSet})\) by the dyadic-measurability of \(\operatorname {rep}\) (Lemma 14.16); \(\operatorname {rep}\) is thus a Borel embedding and the containment follows.
The binary partition is a one-sided generator for the doubling map: \(\bigvee _{n}\operatorname {comap}(T^n)\, \sigma (\alpha )=m_{\mathbb T}\).
The easy inclusion \(\le \) is immediate from measurability of the cells under the iterates. For \(\ge \): each digit set \(T^{-n}(\operatorname {binCell}i)\) is measurable for the saturated \(\sigma \)-algebra, hence each dyadic arc, being a finite intersection of digit sets, is too; reducing Borel to the dyadic-arc family by Theorem 14.17 closes the reverse containment.
The Kolmogorov–Sinai entropy of the doubling map is \(h_\mu (T)=\log 2\).
The generator theorem (Theorem 10.15) collapses the system entropy to the binary partition, since it generates (Theorem 14.18); the per-partition entropy is \(\log 2\) (Theorem 13.17).
For the doubling map,
the genuine full-system Pesin equality on a compact carrier with strictly positive entropy. This is the first non-vacuous full-system instance of the volume-case Pesin formula (Theorem 14.7) in the library: the binary-expansion coding gives a genuine generating partition on a compact space, so both sides are computed rather than degenerate. Its companion Theorem 13.18 exhibits the same equality against the integrated log-Jacobian \(\int \log \left\lvert \det DT \right\rvert \, d\mu =\log 2\).
The system entropy is \(\log 2\) (Theorem 14.19) and the positive-exponent sum of the constant derivative cocycle \((2)\) is \(\log 2\) (Corollary 13.14); the two agree.