σ-algebra glue for the iterated-join filtration σ(B_n)

For a measure-preserving system (α, T, μ) and a finite measurable partition Q, the flat iterated join ksJoin hT Q n (Oseledets.Entropy.KSEntropy) has cell at f : Fin n → κ the cylinder ⋂ₖ<ₙ T^[k]⁻¹(Q_{f k}). Writing σ(B_n) := generatedSigmaAlgebra μ (ksJoin hT Q n) for the σ-algebra generated by these cells, this file proves the three structural "glue" facts about the increasing filtration n ↦ σ(B_n):

1. Monotonicity in n: σ(B_M) ≤ σ(B_n) for M ≤ n.
2. Shift inclusion: comap (T^[a]) σ(B_b) ≤ σ(B_{a+b}) — pulling the b-join σ-algebra back by T^[a] lands inside the (a+b)-join σ-algebra.
3. Sup identity: ⨆ n, σ(B_n) = ⨆ k, comap (T^[k]) σ(Q) — the filtration's supremum is the forward-saturated generating σ-algebra of Q itself.

These are the σ-algebra-saturation glue feeding the Abramov–Rokhlin moving-index conditional Kolmogorov–Sinai limit (issue #13). In particular the sup identity (3) is the bridge that lets a saturation hypothesis ⨆ n, σ(B_n) = 𝒜 be read off from Oseledets.Entropy.factor_iSup_comap_eq, whose left-hand side is ⨆ n, comap (T^[n]) σ(R.pulledBack) — the same forward-saturated shape.

Proof technique

Everything reduces to a single coordinate-cylinder identity (preimage_cells_eq_iUnion, measurableSet_preimage_cells): for k < n and an index i, the single coordinate T^[k]⁻¹(Q_i) is the exact finite union of the n-join cells whose k-th coordinate is i, hence σ(B_n)-measurable. Exactness uses that a MeasurePartition covers the space exactly (MeasurePartition.cover : ⋃ i, cells i = univ), not merely almost everywhere. Each M-join cell (M ≤ n) is a finite intersection of such coordinate cylinders, so it is σ(B_n)-measurable, and generateFrom_le gives lemma 1; the shift T^[a]⁻¹(b-cell) = ⋂ T^[a+l]⁻¹(Q_·) is an intersection of coordinates a..a+b-1 of the (a+b)-join, giving lemma 2 by the same cylinder API together with MeasurableSpace.comap_generateFrom (mirroring Oseledets.Entropy.comap_generatedSigmaAlgebra_pulledBack). Lemma 3 combines the two.

Main results

• Oseledets.Entropy.generatedSigmaAlgebra_ksJoin_mono: σ(B_M) ≤ σ(B_n) for M ≤ n.
• Oseledets.Entropy.comap_iterate_generatedSigmaAlgebra_ksJoin_le: comap (T^[a]) σ(B_b) ≤ σ(B_{a+b}).
• Oseledets.Entropy.iSup_generatedSigmaAlgebra_ksJoin_eq: ⨆ n, σ(B_n) = ⨆ k, comap (T^[k]) σ(Q).

References

• Peter Walters, An Introduction to Ergodic Theory, Graduate Texts in Mathematics 79, Springer (1982), Ch. 4.
• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1–2.

theorem Oseledets.Entropy.preimage_cells_eq_iUnion {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (Q : MeasurePartition μ κ) (n : ℕ) (k : Fin n) (i : κ) : T^[↑k] ⁻¹' Q.cells i = ⋃ (g : { g : Fin n → κ // g k = i }), ksJoinCells Q.cells T n ↑g

Coordinate-cylinder identity for the flat iterated join. For a coordinate k : Fin n and an index i : κ, the single-coordinate cylinder T^[k]⁻¹(Q_i) is the exact union of the n-join cells ⋂ₗ<ₙ T^[l]⁻¹(Q_{g l}) whose k-th coordinate g k equals i: T^[k]⁻¹(Q_i) = ⋃_{g : Fin n → κ, g k = i} (ksJoinCells Q.cells T n g).

⊇ is immediate: each cell with g k = i is contained in its own k-th factor T^[k]⁻¹(Q_{g k}) = T^[k]⁻¹(Q_i). ⊆ uses that Q covers the space exactly (MeasurePartition.cover): given x with T^[k] x ∈ Q_i, choose at every coordinate l an index g l with T^[l] x ∈ Q_{g l}, then overwrite g k := i (consistent, since T^[k] x ∈ Q_i); x lies in the cell at the resulting g.

theorem Oseledets.Entropy.measurableSet_preimage_cells {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (n : ℕ) (k : Fin n) (i : κ) : MeasurableSet (T^[↑k] ⁻¹' Q.cells i)

Single coordinates of the join are σ(B_n)-measurable. Each coordinate cylinder T^[k]⁻¹(Q_i) (for k < n) is, by preimage_cells_eq_iUnion, a finite union of n-join cells, each a generator of generatedSigmaAlgebra μ (ksJoin hT Q n); a finite union of generators is measurable.

theorem Oseledets.Entropy.generatedSigmaAlgebra_ksJoin_mono {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) {M n : ℕ} (hMn : M ≤ n) : generatedSigmaAlgebra μ (ksJoin hT Q M) ≤ generatedSigmaAlgebra μ (ksJoin hT Q n)

Monotonicity of the join σ-algebra in the number of coordinates. For M ≤ n, the σ-algebra σ(B_M) = generatedSigmaAlgebra μ (ksJoin hT Q M) generated by the M-fold join is coarser than σ(B_n): every M-join cell ⋂ₖ<ₘ T^[k]⁻¹(Q_{f k}) is a finite intersection of coordinate cylinders T^[k]⁻¹(Q_{f k}) with k < M ≤ n, each σ(B_n)-measurable (measurableSet_preimage_cells), so the cell is σ(B_n)-measurable and generateFrom_le applies.

theorem Oseledets.Entropy.comap_iterate_generatedSigmaAlgebra_ksJoin_le {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (a b : ℕ) : MeasurableSpace.comap T^[a] (generatedSigmaAlgebra μ (ksJoin hT Q b)) ≤ generatedSigmaAlgebra μ (ksJoin hT Q (a + b))

Shift inclusion of the join σ-algebra. Pulling the b-fold join σ-algebra back by T^[a] lands inside the (a+b)-fold join σ-algebra: comap (T^[a]) σ(B_b) ≤ σ(B_{a+b}).

A generator of comap (T^[a]) σ(B_b) is T^[a]⁻¹ of a b-join cell, i.e. T^[a]⁻¹(⋂ₗ<_b T^[l]⁻¹(Q_{f l})) = ⋂ₗ<_b T^[a+l]⁻¹(Q_{f l}), an intersection of coordinates a, …, a+b-1 of the (a+b)-join, each σ(B_{a+b})-measurable (measurableSet_preimage_cells). MeasurableSpace.comap_generateFrom reduces the comap of generateFrom to a generateFrom of preimages, and generateFrom_le then discharges the goal.

theorem Oseledets.Entropy.generatedSigmaAlgebra_ksJoin_one {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) : generatedSigmaAlgebra μ (ksJoin hT Q 1) = generatedSigmaAlgebra μ Q

The 1-fold join σ-algebra is the generating σ-algebra of Q. The cells of ksJoin hT Q 1 are Q's cells reindexed by the unique equivalence (Fin 1 → κ) ≃ κ (each cell at f : Fin 1 → κ is T^[0]⁻¹(Q_{f 0}) = Q_{f 0}), so the two cell ranges coincide and the generated σ-algebras are equal.

theorem Oseledets.Entropy.iSup_generatedSigmaAlgebra_ksJoin_eq {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Fintype κ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) : ⨆ (n : ℕ), generatedSigmaAlgebra μ (ksJoin hT Q n) = ⨆ (k : ℕ), MeasurableSpace.comap T^[k] (generatedSigmaAlgebra μ Q)

The join filtration saturates the forward-pulled generating σ-algebra of Q. The supremum of the increasing filtration n ↦ σ(B_n) equals the forward-saturated generating σ-algebra of Q: ⨆ n, σ(B_n) = ⨆ k, comap (T^[k]) σ(Q).

≤: each σ(B_n) is below the right-hand side. It suffices to show each n-join cell is (⨆ k, comap (T^[k]) σ(Q))-measurable; the cell is a finite intersection of coordinate cylinders T^[k]⁻¹(Q_·) (k < n), and T^[k]⁻¹(Q_·) ∈ comap (T^[k]) σ(Q) ≤ the supremum.

≥: for each k, comap (T^[k]) σ(Q) = comap (T^[k]) σ(B_1) ≤ σ(B_{k+1}) ≤ ⨆ n, σ(B_n), using generatedSigmaAlgebra_ksJoin_one, the shift inclusion (comap_iterate_… with b = 1), and le_iSup.

This is the bridge to a saturation hypothesis ⨆ n, σ(B_n) = 𝒜: combined with Oseledets.Entropy.factor_iSup_comap_eq (whose left-hand side is the same forward-saturated shape ⨆ n, comap (T^[n]) σ(R.pulledBack)), it lets the moving-index Abramov–Rokhlin limit (issue #13) read off that the join filtration saturates the factor σ-algebra.