The two-sided Kolmogorov–Sinai generator theorem h(e) = h(e, P) #
This file builds the two-sided (invertible) Kolmogorov–Sinai generator theorem: for a
measure-preserving automorphism e : α ≃ᵐ α of a standard Borel probability space and a
two-sided generating finite partition P (Oseledets.Krieger.IsGeneratingTwoSided e P, i.e. the
σ-algebra saturated under both time directions ⨆_{j : ℤ} eʲ σ(P) is the ambient σ-algebra), the
entropy of the system is already attained on P: h(e) = h(e, P).
The classical one-sided generator theorem (Oseledets.Entropy.GeneratorTheorem) requires forward
saturation ⨆_{n : ℕ} (eⁿ)⁻¹ σ(P) = mα, which provably fails for genuine automorphisms such as the
two-sided Bernoulli shift; the correct hypothesis is the two-sided one. This module supplies the
first half of the reduction:
- the symmetric window partition
symWindow e he P Nrepresenting⋁_{j=-N}^{N} eʲ P, realized cleanly as theeᴺ-pullback of the forward(2N+1)-fold join ofP; - the saturation identity
⨆_N σ(symWindow N) = ⨆_{j : ℤ} comap (eʲ) σ(P), so underIsGeneratingTwoSidedthe windows saturate the full σ-algebra; - the window invariance
h(e, symWindow N) = h(e, P)— the genuine invertibility crux, whereebeing an automorphism (MeasurePreserving ⇑e.symm) is used to relabel atoms of a doubly infinite window by the measure-preserving shifteᴺwithout changing entropy.
The window invariance is assembled from two reusable identities (cf. Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), Thm 5; Walkden, Manchester, Lecture 25):
- W2 (iterate invariance)
h(e, R.pullback (ziter e c)) = h(e, R)for anyc : ℤand any partitionR— clean, holding at the level of each entropy-sequence term, no over-counting; this is the one place the negative iterates of the inversee.symmenter. - W1 (block identity)
h(e, ksJoin he P k) = h(e, P)— the standardh(e, ⋁₀^{k-1} e⁻ⁱP) = h(e, P), proved through the exact sequence-level telescopingH(⋁₀^{m-1} e⁻ʲ(⋁₀^{k-1} e⁻ⁱP)) = H(⋁₀^{m+k-2} e⁻ˡP)and a Cesàro shift.
Composing, with symWindow e he P N = (ksJoin he P (2N+1)).pullback (ziter e (-N)):
h(e, symWindow N) = h(e, ksJoin he P (2N+1)) = h(e, P).
References #
- François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §2.
- Charles Walkden, Ergodic Theory (Manchester, MATH41112/61112), Lecture 25.
- Peter Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Ch. 4.
The generated σ-algebra of a pullback partition is the comap of the base. For a
measure-preserving endomorphism T and a finite partition P, the σ-algebra σ(T⁻¹P) generated by
the cells of the pullback partition equals comap T σ(P). (The endomorphism mirror of
Oseledets.Entropy.comap_generatedSigmaAlgebra_pulledBack.)
The symmetric window partition symWindow e he P N, representing the doubly-infinite window
join ⋁_{j=-N}^{N} eʲ P, realized as the eᴺ-pullback of the forward (2N+1)-fold join of P:
its cell at g : Fin (2N+1) → ι is ⋂_{i=0}^{2N} (e^{i-N})⁻¹(P_{g i}). This single clean
pullback-of-ksJoin definition is what makes both the saturation identity and the window-entropy
invariance close (the latter via the iterate-invariance lemma W2 and the block identity W1).
Equations
- Oseledets.Entropy.symWindow e he P N = Oseledets.Entropy.MeasurePartition.pullback ⋯ (Oseledets.Entropy.ksJoin he P (2 * N + 1))
Instances For
Coordinate shift identity. Pulling the forward k-coordinate cylinder (eᵏ)⁻¹A back along
e⁻ᴺ (= ziter e (-N)) shifts it to the two-sided (k-N)-coordinate cylinder
(e^{k-N})⁻¹A. This is the cocycle law ziter_add packaged for set preimages, and is the engine of
both the cell formula symWindow_cell_eq and the coordinate measurability
measurableSet_symWindow_coord.
The cell of symWindow e he P N at g is the two-sided window cylinder
⋂_{i=0}^{2N} (e^{i-N})⁻¹(P_{g i}).
Coordinate measurability for the symmetric window. For |j| ≤ N, written j = k - N with
k : Fin (2N+1), the two-sided coordinate cylinder (e^{k-N})⁻¹(P_i) is measurable with respect to
the σ-algebra generated by symWindow e he P N. Obtained from the one-sided coordinate
measurability measurableSet_preimage_cells of the underlying forward join, pulled back along
e⁻ᴺ through generatedSigmaAlgebra_pullback.
Saturation of the symmetric windows. The supremum over window radii N of the σ-algebras
generated by the symmetric windows equals the two-sided saturated σ-algebra of P:
⨆_N σ(symWindow N) = ⨆_{j : ℤ} comap (ziter e j) σ(P).
Combined with IsGeneratingTwoSided e P (whose content is that the right-hand side is mα), this
shows the symmetric windows saturate the full ambient σ-algebra. The ≤ direction expands each
window cell as a finite intersection of two-sided coordinate cylinders (symWindow_cell_eq), each a
generator of the right-hand side; the ≥ direction realizes each comap (ziter e j) σ(P) inside a
window of radius |j| via the coordinate measurability measurableSet_symWindow_coord.
Entropy is invariant under an injective relabeling with null off-image cells. If ψ : J → I
is injective, the measures match on the image (μ (s (ψ j)) = μ (t j)), and every cell off the
image is μ-null, then entropy μ s = entropy μ t. (The over-counted window-join cells are exactly
the off-image null cells; the consistent ones are the image, in measure-preserving bijection with
the forward-join cells.)
Iterate invariance of the iterated-join entropy sequence (W2, sequence level). For any two-
sided iterate ziter e c, the entropy sequence of the pullback partition (ziter e c)⁻¹ P equals
that of P at every n — no over-counting: the n-fold dynamical join of (ziter e c)⁻¹ P is
exactly the (ziter e c)-pullback of the n-fold join of P (the iterate commutes with e^[k]),
and entropy_pullback then identifies the entropies. This is the one place the negative iterates of
the inverse e.symm enter.
Iterate invariance of the Kolmogorov–Sinai entropy (W2). h(e, (ziter e c)⁻¹ P) = h(e, P):
the Fekete limits agree since the entropy sequences agree termwise
(ksEntropySeq_pullback_ziter).
The block-encode relabeling ψ underlying the block identity W1: a forward (m+K)-join
index h is read as the consistent m-fold join of (K+1)-blocks whose (j, i)-entry is
h (i + j). Its image is exactly the consistent block-join indices; the inconsistent ones index
μ-null over-counted cells.
Equations
- Oseledets.Entropy.blockEncode m K h j i = h ⟨↑i + ↑j, ⋯⟩
Instances For
Block identity, sequence level (W1). For m ≥ 1, the m-fold dynamical-join entropy of the
length-(K+1) block partition ⋁₀^K e⁻ⁱP equals the (m+K)-fold dynamical-join entropy of P:
H(⋁₀^{m-1} e⁻ʲ(⋁₀^K e⁻ⁱP)) = H(⋁₀^{m+K-1} e⁻ˡP). The over-counted block-join cells are reindexed
by blockEncode onto the forward-join cells (an injection whose image is the consistent cells,
their measures matching, the inconsistent cells being μ-null);
entropy_eq_of_injective_of_ae_null then identifies the two entropies.
Block identity (W1). h(e, ⋁₀^K e⁻ⁱP) = h(e, P): the Kolmogorov–Sinai entropy of the system
relative to a length-(K+1) block partition equals that relative to P. The Cesàro limit of the
sequence identity ksEntropySeq_ksJoin_succ: H_block(m)/m = (H_P(m+K)/(m+K)) · ((m+K)/m) for
m ≥ 1, where the first factor converges to h(e, P) (a shift of the Fekete sequence) and the
second to 1.
Window invariance (the invertibility crux). h(e, symWindow N) = h(e, P): the Kolmogorov–
Sinai entropy of the system relative to the symmetric window ⋁_{j=-N}^{N} eʲ P equals that
relative to P. The window is the eᴺ-pullback of the forward (2N+1)-block, so iterate W2
(ksEntropyPartition_pullback_ziter) strips the shift — this is the only step needing e to be an
automorphism — and the block identity W1 (ksEntropyPartition_ksJoin) collapses the block.
The continuity half (L2): conditioning on the growing windowed σ-algebra #
Conditional entropy of a partition measured by the conditioning σ-algebra vanishes. If every
cell of R is 𝒜-measurable (𝒜 ≤ mα), then condEntropy μ 𝒜 R.cells = 0: each 𝒜-measurable
indicator is its own conditional expectation, so the kernel cell masses are 0/1 a.e. and every
negMulLog term vanishes (the 𝒜 ≤ mα generalization of condEntropy_full_eq_zero).
The windowed forward-saturated σ-algebra winSat e he P N: the forward-e-saturation of
the symmetric window symWindow e he P N, i.e. ⨆ n, σ(⋁₀^{n-1} e⁻ᵏ (symWindow N)). It is
forward-e-invariant (comap_winSat_le), increasing in N (winSat_mono), and saturates mα as
N → ∞ under two-sided generation (iSup_winSat_eq); conditioning the Abramov–Rokhlin identity on
it (rather than on mα) lets the relative term vanish by Lévy-upward continuity.
Equations
- Oseledets.Entropy.winSat e he P N = ⨆ (n : ℕ), Oseledets.Entropy.generatedSigmaAlgebra μ (Oseledets.Entropy.ksJoin he (Oseledets.Entropy.symWindow e he P N) n)
Instances For
The windowed σ-algebra is forward-e-invariant: comap (⇑e) (winSat N) ≤ winSat N. Through
iSup_generatedSigmaAlgebra_ksJoin_eq, winSat N = ⨆ k, comap (e^[k]) σ(symWindow N), and pulling
back by e shifts the index k ↦ k+1, staying inside the supremum.
Monotonicity of the window σ-algebra in the radius. For N₁ ≤ N₂, σ(symWindow N₁) ≤ σ(symWindow N₂): every two-sided coordinate cylinder (e^{k-N₁})⁻¹(P_·) of the smaller window has
exponent |k - N₁| ≤ N₁ ≤ N₂, hence is a coordinate of the larger window
(measurableSet_symWindow_coord).
The windowed σ-algebra is monotone in the radius N. Reduces to monotonicity of
σ(symWindow N) (generatedSigmaAlgebra_symWindow_mono), pushed through the forward saturation
iSup_generatedSigmaAlgebra_ksJoin_eq (each comap (e^[k]) · and the supremum are monotone).
The windows saturate the full σ-algebra. Under two-sided generation, ⨆ N, winSat N = mα.
Each winSat N ≤ mα; conversely mα = ⨆ j comap (eʲ) σ(P) = ⨆ N σ(symWindow N) (hgen and the L1
saturation iSup_generatedSigmaAlgebra_symWindow), and σ(symWindow N) = σ(⋁₀ symWindow N) ≤ winSat N (generatedSigmaAlgebra_ksJoin_one at n = 1).
L2 crux — the continuity bound. For a two-sided generating P and any finite partition Q,
h(e, Q) ≤ h(e, P). Conditioning the unconditional Abramov–Rokhlin identity on the forward-
invariant windowed σ-algebra winSat N (not mα) splits h(e, Q ∨ symWindow N) into h(e, symWindow N) + h(e, Q ∨ symWindow N | winSat N); window invariance (W1+W2) collapses the first to
h(e, P), while the relative term is ≤ condEntropy μ (winSat N) Q.cells (the symWindow N part
is winSat N-measurable, contributing 0). As N → ∞, winSat N ↗ mα, so by Lévy continuity
condEntropy μ (winSat N) Q.cells → condEntropy μ mα Q.cells = 0, giving the bound.
The two-sided Kolmogorov–Sinai generator theorem. For a measure-preserving automorphism
e : α ≃ᵐ α of a standard Borel probability space and a two-sided generating finite partition P
(IsGeneratingTwoSided e P), the Kolmogorov–Sinai entropy of the system equals the
partition-relative entropy of P: h(e) = h(e, P).
le_antisymm of the free bound h(e, P) ≤ h(e) (le_ksEntropy) and the reverse, which unfolds the
supremum defining ksEntropy and reduces by iSup_le to the continuity crux
ksEntropyPartition_le_of_isGeneratingTwoSided. Unlike the one-sided generator theorem this needs
no forward saturation; the two-sided saturation hgen is what makes the windowed Abramov–Rokhlin
limit valid, and invertibility enters only through the window-entropy invariance.