The partition-level Abramov–Rokhlin identity (B6a, issue #13)

This file develops the finite-n foundations of the partition-level Abramov–Rokhlin identity (B6a) sorry-free, isolating the one genuinely analytic residual (a Cesàro/martingale σ-convergence) as a single named hypothesis.

The target identity, for a factor map π : (α, T, μ) → (β, S, ν) with 𝒜 = comap π 𝓑_Y and a generating partition P refining the pulled-back partition R.pulledBack, is h(P, T) = h(π⁻¹R, T) + h(P, T | 𝒜).

Roadmap and what is proved here

Write A_n = ⋁_{k<n} T⁻ᵏ P and B_n = ⋁_{k<n} T⁻ᵏ(π⁻¹R). The finite-n decomposition is

1. W1 (refinement collapse) entropy_joinCells_of_refines: when each cell of the finer family t is μ-a.e. contained in a single cell of the coarser partition s, the join entropy collapses, H(s ∨ t) = H(t).
2. The absolute chain rule entropy_join_eq_add_condEntropyGivenPartition (proved in CondChainRule): H(B_n ∨ A_n) = H(B_n) + condEntropyGivenPartition μ B_n A_n.
3. Combining (1) and (2) gives the per-n identity H(A_n) = H(B_n) + cond(B_n, A_n).

All three are proved here sorry-free.

Main results

• Oseledets.Entropy.entropy_joinCells_of_refines (W1): the refinement collapse of join entropy.
• Oseledets.Entropy.entropy_join_eq_of_refines: the per-n identity H(A_n) = H(B_n) + condEntropyGivenPartition μ B_n A_n for a coarsening B_n of A_n.

References

• L. M. Abramov, V. A. Rokhlin, The entropy of a skew product of measure-preserving transformations, Vestnik Leningrad Univ. 17 (1962).
• Peter Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Ch. 4.

W1: the refinement collapse of join entropy.

When the finer family t refines the coarser partition s — meaning each cell t j is μ-almost contained in a single cell s (g j) of s — the join s ∨ t has the same entropy as t alone, because for each j the only nonnull intersection s i ∩ t j is the one at i = g j, which equals t j up to null sets.

theorem Oseledets.Entropy.entropy_joinCells_of_refines {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} (s : ι → Set α) (hs_meas : ∀ (i : ι), MeasurableSet (s i)) (hs_disj : Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s)) (t : κ → Set α) (g : κ → ι) (hrefine : ∀ (j : κ), t j ≤ᵐ[μ] s (g j)) : entropy μ (joinCells s t) = entropy μ t

Refinement collapse of join entropy (W1). Let s : ι → Set α be a finite measurable partition of a measure space (α, μ) (its cells are measurable, pairwise a.e. disjoint, covering the space) and t : κ → Set α a finite measurable family. Suppose t refines s in the sense that there is an assignment g : κ → ι with each cell t j μ-a.e. contained in the cell s (g j). Then the entropy of the join collapses to that of the finer family: H(s ∨ t) = H(t).

For each j, of the ι intersections s i ∩ t j only the one at i = g j is nonnull: it equals t j up to a null set (since t j ⊆ᵐ s (g j)), and every other s i ∩ t j (for i ≠ g j) is null (it lies inside s i ∩ s (g j), an a.e.-disjoint pair of partition cells). Summing negMulLog over the grid ι × κ therefore leaves exactly ∑ⱼ negMulLog (μ (t j)).

The per-n identity: chain rule + W1.

Combining the absolute chain rule entropy_join_eq_add_condEntropyGivenPartition with the refinement collapse W1 yields, for any coarsening B of a partition A, the per-n decomposition H(A) = H(B) + condEntropyGivenPartition μ B A. This is the finite stage of the Abramov–Rokhlin identity (before dividing by n and taking the limit).

theorem Oseledets.Entropy.entropy_join_eq_of_refines {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (B : MeasurePartition μ ι) (A : MeasurePartition μ κ) (g : κ → ι) (hrefine : ∀ (f : κ), A.cells f ≤ᵐ[μ] B.cells (g f)) : entropy μ A.cells = entropy μ B.cells + condEntropyGivenPartition μ B.cells A.cells

The per-n Abramov–Rokhlin identity. Let A and B be finite measurable partitions of a probability space with A a refinement of B (each cell A_f is μ-a.e. contained in a single cell B (g f)). Then the entropy of A splits as the entropy of the coarser B plus the conditional entropy of A given B: H(A) = H(B) + condEntropyGivenPartition μ B.cells A.cells.

The absolute chain rule entropy_join_eq_add_condEntropyGivenPartition gives H(B ∨ A) = H(B) + condEntropyGivenPartition μ B.cells A.cells, and the refinement collapse W1 (entropy_joinCells_of_refines, applicable because B is a partition and A refines it) rewrites H(B ∨ A) = H(A).

Step 4: divide by n and pass to the limit.

The per-n identity divided by n is (1/n) H(A_n) = (1/n) H(B_n) + (1/n) cond(B_n, A_n). The two absolute terms converge to ksEntropyPartition (Fekete, tendsto_ksEntropySeq), so the conditional cell-form term (1/n) condEntropyGivenPartition μ B_n A_n converges to the difference. Assembling the limit identity is then pure Tendsto algebra and uniqueness of limits. The result is stated against a named hypothesis hW3 identifying that limit with the relative entropy condKsEntropyPartition — exactly the residual W3 σ-convergence step (Lévy upward / Cesàro), which is the one analytic input not discharged here.

noncomputable def Oseledets.Entropy.condCellSeq {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {T : α → α} [Fintype ι] [Fintype κ] (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (n : ℕ) : ℝ

The conditional cell-form sequence n ↦ condEntropyGivenPartition μ B_n A_n, the additive- over-cells conditional entropy of the n-fold join A_n = ⋁_{k<n}T⁻ᵏP given the coarser join B_n = ⋁_{k<n}T⁻ᵏQ. This is the term whose Cesàro limit is, by the per-n identity, the difference h(P, T) − h(Q, T).

Equations

• Oseledets.Entropy.condCellSeq hT Q P n = Oseledets.Entropy.condEntropyGivenPartition μ (Oseledets.Entropy.ksJoin hT Q n).cells (Oseledets.Entropy.ksJoin hT P n).cells

theorem Oseledets.Entropy.abramovRokhlin_partition_of_W3 {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] {T : α → α} [Fintype ι] [Fintype κ] (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)) (hW3 : Filter.Tendsto (fun (n : ℕ) => condCellSeq hT Q P n / ↑n) Filter.atTop (nhds (condKsEntropyPartition hm hT hinv P))) : ksEntropyPartition hT P = ksEntropyPartition hT Q + condKsEntropyPartition hm hT hinv P

The Abramov–Rokhlin partition identity, modulo the W3 limit-identity hypothesis. Given the per-n refinement of A_n over B_n (each cell of the P-join is μ-a.e. inside a single cell of the Q-join, witnessed by g n) and the W3 σ-convergence hypothesis hW3 identifying the Cesàro limit of the conditional cell-form sequence with the relative entropy condKsEntropyPartition, the partition-level Abramov–Rokhlin identity holds: h(P, T) = h(Q, T) + h(P, T | 𝒜).

Everything except hW3 is discharged sorry-free: the per-n identity entropy_join_eq_of_refines divided by n, the two Fekete convergences tendsto_ksEntropySeq for A_n and B_n, and limit uniqueness. hW3 is the genuine analytic residual (the increasing σ-algebras σ(B_n) catching up to the fixed factor σ-algebra 𝒜, a martingale/Cesàro step).