Forward iterates of a pulled-back generator saturate the factor σ-algebra

Let π : α → β intertwine the dynamics, π ∘ T = S ∘ π, and let R be a generator of the base system (β, S, ν) (so ⨆ n, comap (S^[n]) σ(R) = mβ). Pulling R back along a measure-preserving π gives the partition π⁻¹R of the source with cells π⁻¹(R.cells). This file proves that the forward T-iterates of the pulled-back generating σ-algebra exactly recover the factor σ-algebra comap π mβ: ⨆ n, comap (T^[n]) σ(π⁻¹R) = comap π mβ.

This is the "the generated sub-σ-algebras σ(B_n) increase to comap π mβ" filtration fact underlying the §5b weak-mixing / relative-product analysis of issue #13: the factor σ-algebra is saturated by the observable R, pulled back and refined under the forward dynamics.

Proof outline (pure σ-algebra algebra)

The identity is an entirely algebraic manipulation of comaps, driven by four Mathlib lemmas:

1. The pulled-back generated σ-algebra is the comap of the base generated σ-algebra: σ(π⁻¹R) = comap π σ(R). The cells of π⁻¹R are π⁻¹(R.cells), so their range is preimage π '' (range R.cells), and comap_generateFrom turns comap π (generateFrom (range R.cells)) into exactly generateFrom (preimage π '' range R.cells).
2. Slide T^[n] past π: comap (T^[n]) (comap π σ(R)) = comap (π ∘ T^[n]) σ(R) by comap_comp, and the intertwining iterate π ∘ T^[n] = S^[n] ∘ π (Semiconj.iterate_right) rewrites this to comap π (comap (S^[n]) σ(R)).
3. Commute comap π past the supremum: ⨆ n, comap π (comap (S^[n]) σ(R)) = comap π (⨆ n, comap (S^[n]) σ(R)) by comap_iSup.
4. Apply the generator hypothesis: ⨆ n, comap (S^[n]) σ(R) = mβ is exactly IsGenerating ν S R, collapsing the right-hand side to comap π mβ.

Main results

• Oseledets.Entropy.comap_generatedSigmaAlgebra_pulledBack: σ(π⁻¹R) = comap π σ(R) — the clean base lemma identifying the pulled-back generated σ-algebra with the comap of the base one.
• Oseledets.Entropy.factor_iSup_comap_eq: ⨆ n, comap (T^[n]) σ(π⁻¹R) = comap π mβ — the forward iterates of the pulled-back generator saturate the factor σ-algebra.

References

• Peter Walters, An Introduction to Ergodic Theory, Graduate Texts in Mathematics 79, Springer (1982), Ch. 4.

theorem Oseledets.Entropy.comap_generatedSigmaAlgebra_pulledBack {α : Type u_1} {β : Type u_2} {ι : Type u_3} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] [Fintype ι] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {π : α → β} (hπ : MeasureTheory.MeasurePreserving π μ ν) (R : MeasurePartition ν ι) : generatedSigmaAlgebra μ (MeasurePartition.pulledBack hπ R) = MeasurableSpace.comap π (generatedSigmaAlgebra ν R)

The pulled-back generated σ-algebra is the comap of the base generated σ-algebra. For a measure-preserving π : α → β and a finite measurable partition R of β, the σ-algebra σ(π⁻¹R) generated by the cells of the pulled-back partition π⁻¹R equals the σ-algebra comap π σ(R) pulled back along π from the σ-algebra generated by R: σ(π⁻¹R) = comap π σ(R).

The cells of π⁻¹R are π⁻¹(R.cells), so their range is preimage π '' (range R.cells) (Set.range_comp'); MeasurableSpace.comap_generateFrom then identifies comap π (generateFrom (range R.cells)) with generateFrom (preimage π '' range R.cells).

theorem Oseledets.Entropy.factor_iSup_comap_eq {α : Type u_1} {β : Type u_2} {ι : Type u_3} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] [Fintype ι] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {T : α → α} {S : β → β} {π : α → β} (hπ : MeasureTheory.MeasurePreserving π μ ν) (hπS : π ∘ T = S ∘ π) (R : MeasurePartition ν ι) (hgenR : IsGenerating ν S R) : ⨆ (n : ℕ), MeasurableSpace.comap T^[n] (generatedSigmaAlgebra μ (MeasurePartition.pulledBack hπ R)) = MeasurableSpace.comap π mβ

Forward iterates of a pulled-back generator saturate the factor σ-algebra. Let π : α → β intertwine the dynamics, π ∘ T = S ∘ π, be measure preserving from (α, μ) to (β, ν), and let R be a generator of the base system (β, S, ν) (IsGenerating ν S R). Then the forward T-iterates of the pulled-back generating σ-algebra σ(π⁻¹R) exactly recover the factor σ-algebra pulled back from the base: ⨆ n, comap (T^[n]) σ(π⁻¹R) = comap π mβ.

The proof is pure σ-algebra algebra. By comap_generatedSigmaAlgebra_pulledBack, σ(π⁻¹R) = comap π σ(R). For each n, comap_comp gives comap (T^[n]) (comap π σ(R)) = comap (π ∘ T^[n]) σ(R), and the intertwining iterate π ∘ T^[n] = S^[n] ∘ π (Function.Semiconj.iterate_right) rewrites this to comap π (comap (S^[n]) σ(R)). Commuting comap π out of the supremum (comap_iSup) and applying the generator hypothesis ⨆ n, comap (S^[n]) σ(R) = mβ collapses the right-hand side to comap π mβ.