The moving-σ-algebra conditional Kolmogorov–Sinai limit (issue #13, capstone)

This file proves the capstone of the Abramov–Rokhlin programme: the moving-index conditional Kolmogorov–Sinai limit. Writing A_n := ksJoin hT P n for the n-fold P-join, σ(B_n) := generatedSigmaAlgebra μ (ksJoin hT Q n) for the increasing filtration generated by the Q-joins, and f_n := condEntropy μ (σ(B_n)) (A_n).cells, the main theorem tendsto_condEntropy_genJoin_div states that the Cesàro average f_n / n of the conditional join entropy against the moving conditioning σ-algebra σ(B_n) converges to the relative Kolmogorov–Sinai entropy condKsEntropyPartition hm hT hinv P = h(P, T | 𝒜), provided the filtration saturates 𝒜, i.e. ⨆ n, σ(B_n) = 𝒜 (the hypothesis hsat). The saturation hypothesis is essential — the statement is false without it (the moving σ-algebra need not catch up to 𝒜).

The proof is a two-sided squeeze h ≤ liminf (f_n / n) and limsup (f_n / n) ≤ h:

• Easy direction (h ≤ liminf). Saturation gives σ(B_n) ≤ 𝒜, so conditioning on the coarser σ(B_n) only increases entropy (condEntropy_mono_of_le): condEntropy μ 𝒜 (A_n).cells ≤ f_n. Dividing by n and passing to the limit with the Fekete convergence tendsto_condKsEntropySeq (whose limit is h) gives h ≤ liminf (f_n / n).

• Hard direction (limsup ≤ h). A blocking / Cesàro–Toeplitz argument. Fix m ≥ 1 and a level M ≥ 1. Peeling n = q·m + r into q blocks of length m (the shifted append subadditivity condEntropy_genJoin_pullback_append_le iterated to the block bound condEntropy_genJoin_block_le), and collapsing each block via the joint pull-back condEntropy_comap_pullback together with the shift inclusion comap_iterate_generatedSigmaAlgebra_ksJoin_le, bounds f_n ≤ q · g_M + (M + 2m)·L where g_M := condEntropy μ (σ(B_M)) (A_m).cells and L := log (card ι). Dividing and taking limsup kills the (M + 2m)·L / n term, leaving limsup (f_n / n) ≤ g_M / m for every M. The fixed-partition Lévy theorem condEntropy_tendsto_iSup then sends g_M → condEntropy μ 𝒜 (A_m).cells (using ⨆ M, σ(B_M) = 𝒜), giving limsup ≤ condEntropy μ 𝒜 (A_m).cells / m for every m ≥ 1; the m-Fekete convergence tendsto_condKsEntropySeq collapses this to limsup ≤ h.

Two corollaries follow:

• tendsto_condCellSeq_div: the discharged W3 hypothesis — the cell-form sequence condCellSeq hT Q P n / n also converges to h(P, T | 𝒜), through the W2 bridge condEntropyGivenPartition_eq_condEntropy_generated.
• abramovRokhlin_partition: the unconditional partition-level identity h(P, T) = h(Q, T) + h(P, T | 𝒜), obtained by feeding the vanishing Cesàro defect (read off from the main theorem and the 𝒜-Fekete limit) into abramovRokhlin_partition_of_defect.

Main results

• Oseledets.Entropy.tendsto_condEntropy_genJoin_div: the moving-σ-algebra conditional KS limit.
• Oseledets.Entropy.tendsto_condCellSeq_div: the cell-form Cesàro limit (W3, discharged).
• Oseledets.Entropy.abramovRokhlin_partition: the unconditional Abramov–Rokhlin partition identity.

References

• Manfred Einsiedler, Elon Lindenstrauss, Thomas Ward, Entropy in Ergodic Theory and Topological Dynamics, Ch. 2 (the blocking / Cesàro–Toeplitz argument).
• Peter Walters, An Introduction to Ergodic Theory, Springer GTM 79 (1982), §4.5.
• L. M. Abramov, V. A. Rokhlin, The entropy of a skew product of measure-preserving transformations, Vestnik Leningrad Univ. 17 (1962).

theorem Oseledets.Entropy.condEntropy_genJoin_pullback_append_le {α : Type u_1} {ι : Type u_2} {ℱ : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype ι] (hℱ : ℱ ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (c a b : ℕ) : condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P (a + b))).cells ≤ condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P a)).cells + condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P b)).cells

Shifted append subadditivity of the conditional iterated-join entropy for an arbitrary sub-σ-algebra ℱ ≤ mα (no invariance hypothesis), with an outer T^[c]-pullback: H(T⁻ᶜ(⋁ₖ₌₀ᵃ⁺ᵇ⁻¹ T⁻ᵏ α) | ℱ) ≤ H(T⁻ᶜ(⋁ₖ₌₀ᵃ⁻¹ T⁻ᵏ α) | ℱ) + H(T⁻⁽ᶜ⁺ᵃ⁾(⋁ₖ₌₀ᵇ⁻¹ T⁻ᵏ α) | ℱ).

This is the c-shifted version of condEntropy_ksJoin_append_le (which is the case c = 0): the T^[c]-pullback of the (a+b)-fold join factors, cell by cell under Fin.appendEquiv, into the join of the T^[c]-pullback of the a-fold join with the T^[c+a]-pullback of the b-fold join (ksJoinCells_append followed by T^[c]⁻¹(T^[a]⁻¹ ·) = T^[c+a]⁻¹ ·), so the conditional join subadditivity condEntropy_join_le bounds it by the sum. The shift c is what lets the blocking argument keep every per-block shift a multiple of the block length m.

theorem Oseledets.Entropy.condEntropy_genJoin_block_le {α : Type u_1} {ι : Type u_2} {ℱ : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype ι] (hℱ : ℱ ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (m r q : ℕ) : condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P (q * m + r))).cells ≤ ∑ j ∈ Finset.range q, condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P m)).cells + condEntropy μ ℱ (MeasurePartition.pullback ⋯ (ksJoin hT P r)).cells

Block bound for the conditional iterated-join entropy against an arbitrary sub-σ-algebra ℱ ≤ mα. Peeling q·m + r into q blocks of length m followed by a remainder block of length r (each peeled with the shifted append subadditivity condEntropy_genJoin_pullback_append_le so that every per-block shift is a multiple of the block length m): H(A_{qm+r} | ℱ) ≤ ∑_{j<q} H(T⁻ʲᵐ A_m | ℱ) + H(T⁻ᵠᵐ A_r | ℱ), writing A_k = ⋁ₗ₌₀^{k-1} T⁻ˡ α.

Proved by induction on q. The base case q = 0 is the identity T^[0]⁻¹ = id. The inductive step front-peels the first block of length m off A_{(q+1)m+r} = A_{m + (qm+r)} (condEntropy_genJoin_pullback_append_le with a = m, b = qm + r), then applies the inductive hypothesis to the T^[m]-pullback of the remaining A_{qm+r} — using the shift parameter c of the helper to absorb the outer T^[m] and shift every inner per-block shift by m.

theorem Oseledets.Entropy.condEntropy_genJoin_block_collapse {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype κ] [Fintype ι] (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (m s n : ℕ) (hsn : s ≤ n) : condEntropy μ (generatedSigmaAlgebra μ (ksJoin hT Q n)) (MeasurePartition.pullback ⋯ (ksJoin hT P m)).cells ≤ condEntropy μ (generatedSigmaAlgebra μ (ksJoin hT Q (n - s))) (ksJoin hT P m).cells

Per-block collapse. For the moving conditioning σ-algebra σ(B_n) = generatedSigmaAlgebra μ (ksJoin hT Q n) and a shift s ≤ n, the conditional entropy of the T^[s]-pullback of the m-fold P-join drops to the conditional entropy of the unshifted m-fold join against the earlier σ-algebra σ(B_{n-s}): H(T⁻ˢ A_m | σ(B_n)) ≤ H(A_m | σ(B_{n-s})).

Two steps. First, conditioning monotonicity condEntropy_mono_of_le against the coarser comap (T^[s]) σ(B_{n-s}) (which sits below σ(B_n) by the shift inclusion comap_iterate_generatedSigmaAlgebra_ksJoin_le, after s + (n - s) = n) only increases the entropy: H(T⁻ˢ A_m | σ(B_n)) ≤ H(T⁻ˢ A_m | comap (T^[s]) σ(B_{n-s})). Second, the joint pull-back condEntropy_comap_pullback evaluates the right side back to H(A_m | σ(B_{n-s})).

theorem Oseledets.Entropy.condEntropy_genJoin_blocking_core {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype κ] [Fintype ι] [Nonempty ι] (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (m M n : ℕ) (hm : 1 ≤ m) : condEntropy μ (generatedSigmaAlgebra μ (ksJoin hT Q n)) (ksJoin hT P n).cells ≤ ↑(n / m) * condEntropy μ (generatedSigmaAlgebra μ (ksJoin hT Q M)) (ksJoin hT P m).cells + ↑(M * m + m) * Real.log ↑(Fintype.card ι)

The blocking core inequality. Fix a block length m ≥ 1 and a level M. For every n, the conditional join entropy f_n = H(A_n | σ(B_n)) against the moving σ-algebra is bounded by q copies of the fixed-level term g_M := H(A_m | σ(B_M)) plus an n-independent ceiling, where q = n / m: H(A_n | σ(B_n)) ≤ (n / m) · H(A_m | σ(B_M)) + (M·m + m) · log (card ι).

This packages the whole blocking argument: the block bound condEntropy_genJoin_block_le peels n = q·m + r into q shifted m-blocks and a remainder; each m-block collapses (condEntropy_genJoin_block_collapse) to H(A_m | σ(B_{n-jm})), which is ≤ g_M for the good blocks (σ(B_M) ≤ σ(B_{n-jm}) when M ≤ n - jm) and ≤ m · log (card ι) (the uniform bound condEntropy_ksJoin_le_nsmul_log_card) for the bad blocks; the bad blocks number at most M (they sit in Ico (q - M) q), and the remainder is ≤ m · log (card ι).

theorem Oseledets.Entropy.tendsto_condEntropy_genJoin_div {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype ι] [Fintype κ] [Nonempty ι] (hm : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hinv : MeasurableSpace.comap T 𝒜 ≤ 𝒜) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (hsat : ⨆ (n : ℕ), generatedSigmaAlgebra μ (ksJoin hT Q n) = 𝒜) : Filter.Tendsto (fun (n : ℕ) => condEntropy μ (generatedSigmaAlgebra μ (ksJoin hT Q n)) (ksJoin hT P n).cells / ↑n) Filter.atTop (nhds (condKsEntropyPartition hm hT hinv P))

The moving-σ-algebra conditional Kolmogorov–Sinai limit (issue #13 capstone). Writing A_n := ksJoin hT P n, σ(B_n) := generatedSigmaAlgebra μ (ksJoin hT Q n) for the increasing filtration generated by the Q-joins, and f_n := condEntropy μ (σ(B_n)) (A_n).cells, the Cesàro average f_n / n of the conditional join entropy against the moving conditioning σ-algebra converges to the relative Kolmogorov–Sinai entropy h(P, T | 𝒜) = condKsEntropyPartition hm hT hinv P, provided the filtration saturates 𝒜, i.e. ⨆ n, σ(B_n) = 𝒜 (the hypothesis hsat).

This is a two-sided squeeze. The easy direction h ≤ liminf (f_n / n): saturation gives σ(B_n) ≤ 𝒜, so conditioning on the coarser σ(B_n) only increases entropy (condEntropy_mono_of_le), condEntropy μ 𝒜 (A_n) ≤ f_n; dividing and using the 𝒜-Fekete limit (tendsto_condKsEntropySeq) gives the bound on the liminf. The hard direction limsup (f_n / n) ≤ h is a blocking / Cesàro–Toeplitz argument: the core inequality condEntropy_genJoin_blocking_core gives f_n ≤ (n/m)·g_M + (M·m+m)·L for g_M := condEntropy μ (σ(B_M)) (A_m); dividing kills the n-independent ceiling in the limsup, leaving limsup ≤ g_M / m; the fixed-partition Lévy theorem condEntropy_tendsto_iSup (with ⨆ M, σ(B_M) = 𝒜) sends g_M → condEntropy μ 𝒜 (A_m), giving limsup ≤ condEntropy μ 𝒜 (A_m) / m for every m ≥ 1, which the m-Fekete limit collapses to limsup ≤ h. The saturation hypothesis hsat is essential — the statement is false without it.

See Einsiedler–Lindenstrauss–Ward, Entropy in Ergodic Theory and Topological Dynamics, Ch. 2, and Walters, GTM 79, §4.5.

theorem Oseledets.Entropy.tendsto_condCellSeq_div {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype ι] [Fintype κ] [Nonempty ι] (hm : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hinv : MeasurableSpace.comap T 𝒜 ≤ 𝒜) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (hsat : ⨆ (n : ℕ), generatedSigmaAlgebra μ (ksJoin hT Q n) = 𝒜) : Filter.Tendsto (fun (n : ℕ) => condCellSeq hT Q P n / ↑n) Filter.atTop (nhds (condKsEntropyPartition hm hT hinv P))

The cell-form Cesàro limit (W3, discharged under saturation). The conditional cell-form sequence condCellSeq hT Q P n / n converges to the relative Kolmogorov–Sinai entropy h(P, T | 𝒜), provided the join filtration saturates 𝒜 (hsat). This discharges the named hypothesis hW3 of abramovRokhlin_partition_of_W3: through the W2 bridge condEntropyGivenPartition_eq_condEntropy_generated, the cell-form sequence equals the σ-algebra conditional join entropy against the moving generated σ-algebra σ(B_n), so the main theorem tendsto_condEntropy_genJoin_div applies verbatim.

theorem Oseledets.Entropy.abramovRokhlin_partition {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Fintype ι] [Fintype κ] [Nonempty ι] (hm : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hinv : MeasurableSpace.comap T 𝒜 ≤ 𝒜) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (g : (n : ℕ) → (Fin n → ι) → Fin n → κ) (hrefine : ∀ (n : ℕ) (f : Fin n → ι), (ksJoin hT P n).cells f ≤ᵐ[μ] (ksJoin hT Q n).cells (g n f)) (hsat : ⨆ (n : ℕ), generatedSigmaAlgebra μ (ksJoin hT Q n) = 𝒜) : ksEntropyPartition hT P = ksEntropyPartition hT Q + condKsEntropyPartition hm hT hinv P

The unconditional Abramov–Rokhlin partition identity (issue #13). Given the per-n refinement of the P-join A_n over the Q-join B_n (each P-join cell is μ-a.e. inside a single Q-join cell, witnessed by g) and the saturation hypothesis hsat : ⨆ n, σ(B_n) = 𝒜, the Kolmogorov–Sinai entropy of P splits as the entropy of the factor Q plus the relative entropy of P over 𝒜: h(P, T) = h(Q, T) + h(P, T | 𝒜).

The Cesàro entropy defect (H(A_n | σ(B_n)) − H(A_n | 𝒜)) / n vanishes: both H(A_n | σ(B_n)) / n (the main theorem tendsto_condEntropy_genJoin_div) and H(A_n | 𝒜) / n = condKsEntropySeq 𝒜 / n (Fekete, tendsto_condKsEntropySeq) converge to h(P, T | 𝒜), so their difference tends to 0. Feeding this defect into abramovRokhlin_partition_of_defect assembles the identity.