9 Kolmogorov–Sinai entropy
Alongside the multiplicative theory of the preceding chapters, the library develops the classical entropy theory of a measure-preserving system: the Shannon entropy of a finite measurable partition, its conditional refinement, the Kolmogorov–Sinai entropy \(h(T)\) as a Fekete limit over iterated joins, and the structural theorems that make it computable — the one- and two-sided generator theorems and the Abramov–Rokhlin addition formula. The chapter closes where the additive and multiplicative theories meet: the Margulis–Ruelle inequality \(h(T)\le \sum _{\lambda _i{\gt}0}\lambda _i\) bounding the entropy by the positive Lyapunov exponents of the derivative cocycle, and Rokhlin’s volume-distortion identity \(h(T,\xi )=\int \log \left\lvert \det DT \right\rvert \, d\mu \).
Throughout, \((\alpha ,\mu )\) is a measure space with \(\mu \) a probability measure, \(T\) a measure-preserving transformation, and partitions are finite, indexed by a Fintype. Where regular conditional probabilities are needed (conditional entropy, the generator theorems, Abramov–Rokhlin), the space is additionally assumed standard Borel. We write \(\eta (t)=-t\log t\) (Mathlib’s \(\operatorname {negMulLog}\), with \(\eta (0)=0\) built in).
9.1 Partitions and Shannon entropy
The Shannon entropy of a finite family of cells \(s:\iota \to \mathcal P(\alpha )\) with respect to a measure \(\mu \) is
the average information gained by learning which cell a \(\mu \)-random point lies in. The definition is on loose data — an arbitrary Fintype-indexed family of sets — so it applies both to genuine partitions and to intermediate non-partition families.
A finite measurable partition of \((\alpha ,\mu )\) is a structure bundling a Fintype-indexed family of cells \(A_i\subseteq \alpha \) together with proofs that each cell is measurable, that the cells are pairwise almost-everywhere disjoint, and that they cover the whole space, \(\bigcup _i A_i=\alpha \).
A finite measurable partition of a probability space into \(k\) cells (with \(k\ge 1\)) has Shannon entropy at most \(\log k\).
The cell measures \(p_i=\mu (A_i)\) sum to \(1\) by finite additivity over the a.e.-disjoint cover. Jensen’s inequality for the concave \(\eta \) with equal weights \(1/k\) gives \(k^{-1}H \le \eta \bigl(\sum _i k^{-1}p_i\bigr) = \eta (1/k) = k^{-1}\log k\), and the positive factor \(k^{-1}\) cancels.
For two finite measurable partitions \(\alpha =(A_i)\) and \(\beta =(B_j)\) of a probability space, the entropy of the join (common refinement) \(\alpha \vee \beta \), whose cell family at \((i,j)\) is the intersection \(A_i\cap B_j\), satisfies
The discrete Gibbs inequality \(\sum _x p_x\log p_x \ge \sum _x p_x\log q_x\) (proved termwise from \(\log (q/p)\le q/p-1\)) is applied to the joint distribution \(p_{(i,j)}=\mu (A_i\cap B_j)\) and the product distribution \(q_{(i,j)}=\mu (A_i)\mu (B_j)\). The marginal identities \(\sum _j p_{(i,j)}=\mu (A_i)\) and \(\sum _i p_{(i,j)}=\mu (B_j)\) make both vectors probability vectors and expand \(-\sum p_{(i,j)}\log q_{(i,j)}\) into exactly \(H(\alpha )+H(\beta )\).
For a measure-preserving \(T\) and a finite measurable partition \(\beta \), the pullback partition \(T^{-1}\beta \) with cells \(T^{-1}B_j\) has the same Shannon entropy as \(\beta \): \(H(T^{-1}\beta )=H(\beta )\).
Each cell measure is preserved, \(\mu (T^{-1}B_j)=\mu (B_j)\), so the corresponding \(\eta \)-terms agree summand by summand.
9.2 Conditional entropy
On a standard Borel probability space, the conditional Shannon entropy of a finite family of cells \(s\) given a sub-\(\sigma \)-algebra \(\mathcal A\) is
the \(\mu \)-average of the pointwise entropy computed against the regular conditional probability kernel \(\kappa =\operatorname {condExpKernel}\mu \, \mathcal A\). It measures the information about the partition remaining after conditioning on \(\mathcal A\); conditioning on the trivial \(\sigma \)-algebra recovers the ordinary entropy.
For any finite measurable partition \(P\) of a standard Borel probability space and any sub-\(\sigma \)-algebra \(\mathcal A\le m_\alpha \),
Jensen’s inequality for the concave \(\eta \), applied cell by cell: the \(\mu \)-average of \(\eta (\kappa _\omega (P_i))\) is at most \(\eta \) of the average \(\int \kappa _\omega (P_i)\, d\mu (\omega )\), which the disintegration identity \(\int \kappa _\omega (P_i)\, d\mu = \mu (P_i)\) turns into \(\eta (\mu (P_i))\). Summing over \(i\) gives the bound.
9.3 Kolmogorov–Sinai entropy as a Fekete limit
For a measure-preserving \(T\) and a finite measurable partition \(\alpha \), the iterated join \(\bigvee _{k=0}^{n-1}T^{-k}\alpha \) is realized as the partition indexed by the flat function type \(\operatorname {Fin}n\to \iota \), whose cell at \(f\) is the intersection \(\bigcap _{k{\lt}n} T^{-k}\bigl(\alpha _{f(k)}\bigr)\). Cells are measurable as finite intersections of preimages under the iterates \(T^k\), pairwise a.e. disjoint (two distinct indices disagree at some coordinate \(k\), where measure-preservation of \(T^k\) transports the disjointness of \(\alpha \)), and cover the space. For \(n=0\) this is the trivial one-cell partition.
The iterated-join entropy sequence of \((T,\alpha )\) is
the Shannon entropy of the flat \(n\)-fold join. Its term at \(0\) is \(0\), and every term is nonnegative.
For a measure-preserving \(T\) on a probability space and all \(n,m\),
Splitting the index type along \(\operatorname {Fin}n\oplus \operatorname {Fin}m\simeq \operatorname {Fin}(n+m)\) exhibits, cell by cell, the \((n+m)\)-fold join as the ordinary join of the \(n\)-fold join with the \(T^n\)-pullback of the \(m\)-fold join. Join subadditivity (Theorem 9.4) bounds the entropy by the sum of the two join entropies, and pullback invariance (Lemma 9.5) — \(T^n\) is measure-preserving — identifies the second summand with the \(m\)-fold join entropy.
The Kolmogorov–Sinai entropy of \(T\) relative to a finite partition \(\alpha \) is the Fekete limit of the subadditive iterated-join entropy sequence,
packaged through Mathlib’s \(\texttt{Subadditive.lim}\) (an infimum of the averaged terms, so the definition is total).
The averaged iterated-join entropies converge: \(\frac1n H\bigl(\bigvee _{k{\lt}n}T^{-k}\alpha \bigr)\to h(T,\alpha )\) as \(n\to \infty \).
Fekete’s subadditivity lemma (\(\texttt{Subadditive.tendsto\_ lim}\)) applied to the sequence of Theorem 9.10; its boundedness-below hypothesis is discharged from the nonnegativity of the entropies, each averaged term being at least \(0\).
The Kolmogorov–Sinai entropy of the system is the supremum of the partition-relative entropies over all finite measurable partitions,
taken in the complete lattice \(\overline\mathbb {R}=[-\infty ,+\infty ]\) (EReal) so that the definition is total even when the entropy is infinite. The supremum ranges over \(\operatorname {Fin}n\)-indexed partitions for every \(n\in \mathbb {N}\), which by reindexing invariance realizes the full partition supremum; each \(h(T,\alpha )\) is below \(h(T)\) (), and \(h(T)\ge 0\), witnessed by the trivial one-cell partition.
9.4 The generator theorems
Computing \(h(T)\) from the definition requires exhausting all finite partitions. The Kolmogorov–Sinai generator theorem collapses the supremum to a single partition, provided that partition generates the full \(\sigma \)-algebra under the dynamics.
A finite measurable partition \(P\) is (one-sided) generating for \((\alpha ,T,\mu )\) if the forward-saturated \(\sigma \)-algebra it generates is the ambient one:
where \(\sigma (P)\) is the \(\sigma \)-algebra generated by the cells of \(P\). This is the standard generator condition for a (possibly non-invertible) endomorphism: the whole measurable structure is recovered from the observable \(P\) and its forward time-translates.
Let \(T\) be a measure-preserving transformation of a standard Borel probability space and \(P\) a one-sided generating finite partition. Then the entropy of the system is attained on \(P\):
No ergodicity is required; standard Borelness and the probability hypothesis feed the kernel disintegration, and the saturation supplied by the generating hypothesis is load-bearing.
By \(\le \)-antisymmetry; \(h(T,P)\le h(T)\) is free from the defining supremum. For the converse it suffices to bound \(h(T,Q)\le h(T,P)\) for every finite partition \(Q\). Apply the unconditional Abramov–Rokhlin partition identity (Theorem 9.20) to the refinement \(R=Q\vee P\) over the factor \(P\), conditioning on the full \(\sigma \)-algebra: the conditional entropy against \(m_\alpha \) vanishes (each kernel cell mass is a.e. \(0\) or \(1\), and \(\eta \) kills both), the generating hypothesis supplies the saturation \(\bigvee _n\sigma (P\text{-join})=m_\alpha \) that the moving-index limit needs, and each \((Q\vee P)\)-join cell lies inside a single \(P\)-join cell. Hence \(h(T,Q)\le h(T,Q\vee P)=h(T,P)+0\).
For a measure-preserving automorphism \(e:\alpha \simeq \alpha \), a finite partition \(P\) is two-sided generating if the \(\sigma \)-algebra saturated under both time directions is the ambient one:
This is the correct condition for invertible systems: forward one-sided generation is strictly stronger and provably fails for genuine automorphisms such as the two-sided Bernoulli shift.
Let \(e\) be a measure-preserving automorphism of a standard Borel probability space and \(P\) a two-sided generating finite partition. Then
Again by reduction to \(h(e,Q)\le h(e,P)\) for arbitrary \(Q\), but along the symmetric windows \(\bigvee _{j=-N}^{N}e^{j}P\), realized as the \(e^{N}\)-pullback of the forward \((2N{+}1)\)-fold join. Invertibility enters exactly once, in the window-entropy invariance \(h(e,\bigvee _{-N}^{N}e^{j}P)=h(e,P)\), assembled from the iterate invariance \(h(e,e^{-c}R)=h(e,R)\) (\(c\in \mathbb {Z}\), using the inverse \(e^{-1}\)) and the block identity \(h(e,\bigvee _{0}^{k-1}e^{-i}P)=h(e,P)\) via a sequence-level telescoping and a Cesàro shift. Conditioning \(Q\) on the increasing window \(\sigma \)-algebras and letting \(N\to \infty \), the relative term vanishes by Lévy-upward continuity since the windows saturate \(m_\alpha \) by the two-sided generating hypothesis, leaving \(h(e,Q)\le h(e,P)\).
9.5 The Abramov–Rokhlin addition formula
For a sub-\(\sigma \)-algebra \(\mathcal A\le m_\alpha \) with \(T^{-1}\mathcal A\le \mathcal A\) (forward invariance), the relative entropy of \(T\) on a partition \(\alpha \) given \(\mathcal A\) is the Fekete limit of the conditional iterated-join entropies,
the conditional sequence being subadditive by the conditional analogues of Theorem 9.4 and Lemma 9.5.
The relative entropy of the system given \(\mathcal A\) is the \(\overline\mathbb {R}\)-valued supremum \(h(T\mid \mathcal A) = \sup _\alpha h(T,\alpha \mid \mathcal A)\) over all finite measurable partitions, mirroring Definition 9.13.
Let \(T\) preserve \(\mu \) on a standard Borel probability space, let \(\mathcal A\le m_\alpha \) be forward invariant, and let \(P, Q\) be finite partitions such that (i) each cell of the \(n\)-fold \(P\)-join lies \(\mu \)-a.e. inside a single cell of the \(n\)-fold \(Q\)-join (a refinement witness \(g\)), and (ii) the join filtration of \(Q\) saturates \(\mathcal A\): \(\bigvee _n \sigma \bigl(\bigvee _{k{\lt}n}T^{-k}Q\bigr)=\mathcal A\). Then
The saturation hypothesis is essential: the identity is false without it.
Per \(n\), the refinement collapses the join \(H(A_n\vee B_n)\) to \(H(B_n)\) plus the conditional term, and the finite conditional chain rule expresses \(H(A_n) = H(B_n) + H(A_n\mid \sigma (B_n))\) for the join partitions \(A_n=\bigvee _{k{\lt}n}T^{-k}P\), \(B_n=\bigvee _{k{\lt}n}T^{-k}Q\). Dividing by \(n\), the first two averaged terms converge to \(h(T,P)\) and \(h(T,Q)\) by Fekete. For the conditional term the conditioning \(\sigma \)-algebra moves with \(n\); a martingale (Lévy-upward) \(\sigma \)-convergence argument, valid under the saturation (ii), shows the Cesàro defect between conditioning on \(\sigma (B_n)\) and on the fixed limit \(\mathcal A\) vanishes, so the moving conditional average converges to \(h(T,P\mid \mathcal A)\).
Let \(\pi :(\alpha ,T,\mu )\to (\beta ,S,\nu )\) be a factor map of measure-preserving systems on probability spaces (\(\alpha \) standard Borel), and let \(P, R\) be finite partitions of the total and factor systems, supplied with the generator reductions \(h(T)=h(T,P)\), \(h(S)=h(S,R)\), the relative-generator reduction \(h(T\mid \pi ^{-1}\mathcal B_\beta )=h(T,P\mid \pi ^{-1}\mathcal B_\beta )\), and the partition-level identity of Theorem 9.20 for \(P\) over \(\pi ^{-1}R\). Then the entropy of the total system splits as
the factor entropy plus the fibrewise entropy relative to the pulled-back factor \(\sigma \)-algebra \(\pi ^{-1}\mathcal B_\beta =\operatorname {comap}\pi \, m_\beta \).
Pure \(\overline\mathbb {R}\)-algebra threading three proved ingredients: rewrite \(h(T)=h(T,P)\) by the generator reduction, expand by the partition-level identity into \(h(T,\pi ^{-1}R)+h(T,P\mid \pi ^{-1}\mathcal B_\beta )\), identify \(h(T,\pi ^{-1}R)=h(S,R)\) by the factor-relative invariance (entropies of pulled-back joins agree cell-measure by cell-measure since \(\pi \) intertwines the dynamics and pushes \(\mu \) to \(\nu \)), and fold back with the two remaining reductions. In the sharpened form \(\texttt{abramov\_ rokhlin\_ of\_ W3}\) the partition identity is discharged down to the single martingale \(\sigma \)-convergence input, and when \(R\) generates the base (\(\texttt{IsGenerating}\ \nu \ S\ R\)) that too is proved, making the formula unconditional.
9.6 The Margulis–Ruelle inequality and Rokhlin’s formula
The bridge back to the multiplicative theory of Chapters 2–6: for a smooth ergodic self-map \(T\) of \(\mathbb {R}^d\) (as EuclideanSpace), the derivative cocycle \(x\mapsto D_xT\) satisfies the standing hypotheses of the multiplicative ergodic theorem, and its Lyapunov exponents \(\lambda _1\ge \dots \ge \lambda _d\) (Definition 6.11) control the Kolmogorov–Sinai entropy from above.
Let \(T\) be an ergodic self-map of \(\mathbb {R}^d\) with everywhere-nonsingular derivative cocycle and one-sided log-integrable derivative data (Definition 2.4 for \(DT\) and \(DT^{-1}\)), and suppose the geometric atom-counting bound holds: every finite partition \(\alpha \) satisfies \(h(T,\alpha )\le \sum _{\lambda _i{\gt}0}\lambda _i\), the sum of the strictly positive Lyapunov exponents of the derivative cocycle (a deterministic constant, the spectrum being a.e. constant by ergodicity). Then the system entropy obeys
The pure lattice step: unfold the defining double supremum of \(h(T)\) over arities \(n\) and \(\operatorname {Fin}n\)-indexed partitions, and apply \(\texttt{iSup\_ le}\) twice in \(\overline\mathbb {R}\) to the uniform per-partition hypothesis. The content of this node is the exact interface: everything around the genuinely geometric per-partition estimate is proved.
Same setting (ergodic \(T\) on \(\mathbb {R}^d\), nonsingular log-integrable derivative cocycle). Assume only the honest non-compactness input — the Mañé/Katok geometric atom count: for every finite partition \(P\) there are \(\varepsilon {\gt}0\) and \(C\ge 0\) such that, \(\mu \)-a.e., the number of atoms of the \(n\)-fold refinement meeting an orbit eventually satisfies
the \(\varepsilon \)-covering number of the image ellipsoid. Then
Some such distortion hypothesis is unavoidable on the noncompact phase space: the bare inequality is false in general (Riquelme 2017).
The one-step sharp anisotropic covering count \(\mathcal N_\varepsilon \bigl(L\, \overline B(0,\varepsilon )\bigr)\le 6^d\prod _i\max (1,\sigma _i(L))\) is proved in-tree by a constructive SVD ellipsoid domination, and is composed with the assumed atom count to bound the atom growth by the positive singular-value product \(\prod _i\max (1,\sigma _i(D_xT^{n}))\). Along a.e. orbit, \(\frac1n\log \) of that product tends to \(\sum \lambda _i^{+}\) by the multiplicative ergodic theorem (Theorem 5.30); the \(\log \)-cardinality bound passes through the Fekete limit to give \(h(T,P)\le \sum _{\lambda _i{\gt}0}\lambda _i\) per partition, and Theorem 9.22 folds the supremum.
Let \(T\) be a measure-preserving, differentiable self-map of \(\mathbb {R}^d\) with \(\mu \ll \mathrm{vol}\), everywhere-nonsingular derivative, a one-sided generating finite partition \(\xi \) on whose cells \(T\) is injective, and \(\mu \)-integrable \(\log \rho \) (\(\rho \) the density \(d\mu /d\mathrm{vol}\)) and \(\log \left\lvert \det DT \right\rvert \). Then the per-partition entropy is the integrated volume distortion:
Together with the determinant identity of Theorem 6.20, the right-hand side is the sum \(\sum _i\lambda _i\) of all Lyapunov exponents of the derivative cocycle — so for expanding maps (all exponents positive) this saturates the Margulis–Ruelle bound, giving Pesin’s entropy formula in that regime.
Three identities composed. First, the sharp-rate form of the Fekete limit expresses \(h(T,\xi )\) as the conditional entropy \(H\bigl(\xi \mid \bigvee _k\sigma (T^{-1}\xi \text{-joins})\bigr)\) of the partition against its own strict future. Second, the generating hypothesis glues that future \(\sigma \)-algebra to \(\operatorname {comap}T\, m_\alpha \). Third, Coudène’s conditional-expectation computation evaluates \(H(\xi \mid T^{-1}m_\alpha )\) by the change-of-variables formula on each injectivity cell, producing \(\int \log \left\lvert \det (D_xT) \right\rvert \, d\mu \); a final bridge identifies the Fréchet-derivative determinant with the determinant of the matrix derivative cocycle. An instantiated equality (the doubling map on the circle) is exhibited elsewhere in the library.