Conditional entropy along a σ-saturating partition sequence tends to zero

This file proves the abstract glue lemma SL3 for the product-entropy upper bound h(T × id) ≤ h(T) (Walters, An Introduction to Ergodic Theory, Theorem 4.23) of GitHub issue #20: for a fixed finite measurable partition P of a standard-Borel probability space and an increasing sequence of finite partitions B n whose generated σ-algebras saturate the ambient σ-algebra (⨆ n σ(B n) = mα), the conditional Shannon entropies H(P | σ(B n)) converge to 0.

The lemma is purely an analytic glue step: the actual "rectangle saturation" content (⨆ n σ(B n) = mα) is supplied at assembly, where B n is a sequence of product rectangles on X × Y built from coordinate cylinders on a two-sided shift and dyadic partitions of [0, 1). Crucially, that saturation is static (it is the standard generation of the product σ-algebra), so this route side-steps the two-sided forward-generator wall entirely.

Proof outline

Two ingredients suffice:

• Lévy-upward continuity (condEntropy_tendsto_iSup): along the increasing sequence of conditioning σ-algebras 𝒜 n := σ(B n), the conditional entropies H(P | 𝒜 n) converge to the conditional entropy H(P | ⨆ n, 𝒜 n) with respect to the limiting σ-algebra.
• Vanishing at the full σ-algebra (condEntropy_full_eq_zero): conditioning on the whole ambient σ-algebra mα makes every cell mass a.e. {0, 1}-valued, so H(P | mα) = 0.

Substituting the saturation hypothesis ⨆ n, σ(B n) = mα into the Lévy limit and applying the vanishing lemma identifies the limit value as 0.

Main results

• Oseledets.Entropy.tendsto_condEntropy_genJoin_seq_zero: H(P | σ(B n)) → 0 along a σ-saturating increasing partition sequence.

References

• Peter Walters, An Introduction to Ergodic Theory, Springer GTM 79, Chapter 4 (Thm 4.23).

theorem Oseledets.Entropy.tendsto_condEntropy_genJoin_seq_zero {α' : Type u_1} [mα' : MeasurableSpace α'] [StandardBorelSpace α'] {μ' : MeasureTheory.Measure α'} [MeasureTheory.IsProbabilityMeasure μ'] {ι : Type u_2} [Fintype ι] [Nonempty ι] (P : MeasurePartition μ' ι) (B : ℕ → (k : ℕ) × MeasurePartition μ' (Fin k)) (hmono : Monotone fun (n : ℕ) => generatedSigmaAlgebra μ' (B n).snd) (hsat : ⨆ (n : ℕ), generatedSigmaAlgebra μ' (B n).snd = mα') : Filter.Tendsto (fun (n : ℕ) => condEntropy μ' (generatedSigmaAlgebra μ' (B n).snd) P.cells) Filter.atTop (nhds 0)

SL3 — conditional entropy along a σ-saturating partition sequence tends to zero.

For a fixed finite measurable partition P of a standard-Borel probability space and a sequence B : ℕ → Σ k, MeasurePartition μ' (Fin k) of finite partitions whose generated σ-algebras form an increasing chain (hmono) saturating the ambient σ-algebra (hsat : ⨆ n, σ(B n) = mα'), the conditional Shannon entropies H(P | σ(B n)) converge to 0.

This is the analytic glue step of the product-entropy upper bound h(T × id) ≤ h(T) (Walters, Theorem 4.23): the rectangle-saturation content ⨆ n σ(B n) = mα' is supplied at assembly. The proof combines Lévy-upward continuity of conditional entropy (condEntropy_tendsto_iSup, giving the limit H(P | ⨆ n σ(B n))) with the vanishing of conditional entropy against the full σ-algebra (condEntropy_full_eq_zero), the saturation hypothesis rewriting ⨆ n σ(B n) to mα'.