The finite-entropy countable two-sided generator (Krieger sub-problem A)

This file constructs the countable two-sided generator of finite static entropy that opens the unconditional Krieger finite generator theorem (issue #15). Following Downarowicz, Entropy in Dynamical Systems, Theorem 4.2.3, first half (and the elementary Keane–Serafin proof of Rokhlin's countable generator theorem), the proof of the finite generator theorem first reduces to producing a countable partition Q of the standard-Borel probability space (α, μ) that

• two-sidedly generates mod 0 under the ergodic aperiodic automorphism e (IsGeneratingTwoSidedMod0c e Q, the Countable-indexed analogue of the Fintype-indexed Oseledets.Krieger.IsGeneratingTwoSidedMod0 of Coding.lean), and
• has finite static (Shannon) entropy — formalized, as in Oseledets.Krieger.CountableEntropy, as Summable (fun i => Real.negMulLog (μ (Q i)).toReal) (whence cHμ μ Q is a genuine finite sum).

Only then is Q coded into Fin k (the M1+M2 Rokhlin-tower / name-count combinatorics already in Oseledets.Krieger.Coding/NameCount/RokhlinTower); this file is the static input, not the coding step.

The Countable-indexed coding layer

The mod-0 coding development of Coding.lean is stated for a Fintype-indexed Oseledets.Entropy.MeasurePartition. Since the generator Q is countably infinite, this file re-establishes the few structural facts at the level of a bare Countable-indexed family of cells Q : κ → Set α (we never need the partition axioms for the generation statement — only that each cell is measurable, supplied where used). Concretely:

• ctwoSidedSat e Q := ⨆ n : ℤ, comap (ziter e n) (generateFrom (range Q)) — the two-sided itinerary σ-algebra of the countable family Q;
• IsGeneratingTwoSidedMod0c e Q := mα ≤ eventuallyMeasurableSpace (ctwoSidedSat e Q) (ae μ) — Q two-sidedly generates mod 0.

The two structural lemmas of Coding.lean that the reduction needs — shift-invariance of the two-sided saturation and mod-0 monotonicity under recovery — are re-proved verbatim for the Countable index (their proofs never used Fintype).

The structural reduction (the formalizable core)

The Keane–Serafin / Downarowicz construction produces, inductively, an increasing sequence of finite partitions Qₖ such that

1. each Qₖ ⪯ Qₖ₊₁ refines the previous (σ(Qₖ) ≤ σ(Qₖ₊₁));
2. the two-sided join of Qₖ recovers the k-th standard-Borel generating set Bₖ mod 0 (Bₖ ∈ ⋁ₙ eⁿσ(Qₖ), mod 0); and
3. the static entropies are uniformly bounded, sup_k H(Qₖ) ≤ h(e) + 1 < ∞.

This file proves, unconditionally and sorry-free, the structural step that turns any such sequence into the desired countable generator:

• the limit partition Q := ⋁ₖ Qₖ is realized as a Countable-indexed family whose generated σ-algebra is the supremum ⨆ₖ σ(Qₖ) (generateFrom_limitFamily);
• its two-sided saturation contains every Bₖ mod 0 hence — B generating mα — generates mod 0 (isGeneratingTwoSidedMod0c_limit);
• a uniform entropy bound sup_k H(Qₖ) < ∞ together with a summable index-mass envelope certifies finite static entropy via Oseledets.Krieger.cHμ_summable_of_summable_index_mul.

What is supplied vs. proved

The single dynamical input — the per-step Keane–Serafin refinement lemma (which uses the Shannon–McMillan–Breiman theorem and Rokhlin's lemma to bound the entropy increment) — is not re-derived here; it is exposed as the hypothesis bundle KeaneSerafinData so that the headline existence theorem exists_countable_twoSided_generator_of_keaneSerafinData is a faithful, honest reduction: given the inductive sequence with its three properties, the finite-entropy countable two-sided generator exists. The hard analytic content (SMB + Rokhlin) is isolated in KeaneSerafinData and tracked as the open residual for sub-problem A.

References

• Tomasz Downarowicz, Entropy in Dynamical Systems, Cambridge (2011), §4.2 (Theorem 4.2.3).
• Michael S. Keane and Jacek Serafin, On the countable generator theorem, Fund. Math. 157 (1998), 255–259 (the elementary proof of Rokhlin's countable generator theorem).
• Vladimir Rokhlin, Generators in ergodic theory, II, Vestnik Leningrad. Univ. (1965).
• Eli Glasner, Ergodic Theory via Joinings, Math. Surveys Monogr. 101, AMS (2003).

The Countable-indexed two-sided saturation and mod-0 generation

These mirror twoSidedSat / IsGeneratingTwoSidedMod0 of Coding.lean, but on a bare Countable-indexed family of cells Q : κ → Set α rather than a Fintype-indexed MeasurePartition. The static σ-algebra is generateFrom (range Q).

@[reducible]

noncomputable def Oseledets.Krieger.ctwoSidedSat {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (Q : κ → Set α) : MeasurableSpace α

The two-sided itinerary σ-algebra of a countable family of cells Q : κ → Set α under the automorphism e: the supremum over all integer iterates eⁿ of the pulled-back static σ-algebra σ(Q) = generateFrom (range Q). This is the Countable-indexed analogue of Oseledets.Krieger.twoSidedSat.

Equations

• Oseledets.Krieger.ctwoSidedSat e Q = ⨆ (n : ℤ), MeasurableSpace.comap (Oseledets.Krieger.ziter e n) (MeasurableSpace.generateFrom (Set.range Q))

@[simp]

theorem Oseledets.Krieger.ctwoSidedSat_def {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (Q : κ → Set α) : ctwoSidedSat e Q = ⨆ (n : ℤ), MeasurableSpace.comap (ziter e n) (MeasurableSpace.generateFrom (Set.range Q))

theorem Oseledets.Krieger.comap_ctwoSidedSat_le {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (Q : κ → Set α) (m : ℤ) : MeasurableSpace.comap (ziter e m) (ctwoSidedSat e Q) ≤ ctwoSidedSat e Q

Shift-invariance of the countable two-sided saturation (cf. comap_twoSidedSat_le). Pulling ctwoSidedSat e Q back by any iterate eᵐ lands inside it again, because the reindexing n ↦ n + m is a bijection of ℤ (ziter_add).

def Oseledets.Krieger.IsGeneratingTwoSidedMod0c {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] (μ : MeasureTheory.Measure α) (e : α ≃ᵐ α) (Q : κ → Set α) : Prop

Q two-sidedly generates (α, e, μ) mod 0 for a countable family Q : κ → Set α when the ambient σ-algebra mα is contained in the μ-completion of the two-sided Q-saturation. The Countable-indexed analogue of Oseledets.Krieger.IsGeneratingTwoSidedMod0.

Equations

• Oseledets.Krieger.IsGeneratingTwoSidedMod0c μ e Q = (mα ≤ eventuallyMeasurableSpace (Oseledets.Krieger.ctwoSidedSat e Q) (MeasureTheory.ae μ))

theorem Oseledets.Krieger.comap_eventuallyMeasurableSpace_ctwoSidedSat_le {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (Q : κ → Set α) (m : ℤ) : MeasurableSpace.comap (ziter e m) (eventuallyMeasurableSpace (ctwoSidedSat e Q) (MeasureTheory.ae μ)) ≤ eventuallyMeasurableSpace (ctwoSidedSat e Q) (MeasureTheory.ae μ)

Mod-0 shift-invariance of the countable two-sided saturation (cf. comap_eventuallyMeasurableSpace_twoSidedSat_le). Preimage under a measure-preserving eᵐ commutes with the μ-completion, and shift-invariance is literal, so completion-monotonicity finishes.

The cross-layer coding predicate: a countable generator coded by a Fintype partition

Krieger's construction codes the countable finite-entropy generator Q : κ → Set α (sub-problem A, exists_countable_twoSided_generator) into a Fin k/Fintype partition P (sub-problem B, the Rokhlin-tower / name-count combinatorics). The two saturation layers therefore meet here: Q lives in the Countable layer (ctwoSidedSat, IsGeneratingTwoSidedMod0c) while P lives in the Fintype layer of Coding.lean (twoSidedSat, IsGeneratingTwoSidedMod0). The bridge is the cross-layer coding predicate CodesTwoSidedMod0c e Q P: every cell of the countable Q is recovered, mod 0, by the two-sided P-itinerary of the finite partition. From it the cross-layer recovery (IsGeneratingTwoSidedMod0c.of_codesc) promotes a mod-0 countable two-sided generator Q to the mod-0 finite two-sided generator P — the exact step the headline assembly needs.

def Oseledets.Krieger.CodesTwoSidedMod0c {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_3} [Fintype ι] (e : α ≃ᵐ α) (Q : κ → Set α) (P : Entropy.MeasurePartition μ ι) : Prop

The cross-layer mod-0 coding predicate. A Fintype-indexed (Fin k-valued) partition P : MeasurePartition μ ι codes a countable family of cells Q : κ → Set α two-sidedly mod 0 under e when every cell of Q is recovered, up to a μ-null set, by the two-sided P-itinerary: generateFrom (range Q) ≤ eventuallyMeasurableSpace (twoSidedSat e P) (ae μ).

The left-hand σ-algebra is the static σ-algebra σ(Q) = generateFrom (range Q) of the countable family — exactly the n = 0 term of ctwoSidedSat e Q, matching how IsGeneratingTwoSidedMod0c and ctwoSidedSat are phrased. The right-hand side is the μ-completion of the finite partition's two-sided saturation Oseledets.Krieger.twoSidedSat. This is the conclusion of the symbolic block code: off a null set, the two-sided P-itinerary of a point determines its Q-name, hence which Q-cell it lies in.

Equations

• Oseledets.Krieger.CodesTwoSidedMod0c e Q P = (MeasurableSpace.generateFrom (Set.range Q) ≤ eventuallyMeasurableSpace (Oseledets.Krieger.twoSidedSat e P) (MeasureTheory.ae μ))

theorem Oseledets.Krieger.ctwoSidedSat_mono_of_codesc {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_3} [Fintype ι] (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (P : Entropy.MeasurePartition μ ι) (Q : κ → Set α) (hrec : MeasurableSpace.generateFrom (Set.range Q) ≤ eventuallyMeasurableSpace (twoSidedSat e P) (MeasureTheory.ae μ)) : ctwoSidedSat e Q ≤ eventuallyMeasurableSpace (twoSidedSat e P) (MeasureTheory.ae μ)

Cross-layer mod-0 recovery / refinement monotonicity. If every cell of the countable family Q is recovered mod 0 by the two-sided saturation of the finite partition P (σ(Q) ≤ completion (twoSidedSat e P)), then the entire countable two-sided saturation of Q is contained in that completion: ctwoSidedSat e Q ≤ completion (twoSidedSat e P).

Each ℤ-term comap (eᵐ) σ(Q) of ctwoSidedSat e Q is bounded, by comap-monotonicity in the hypothesis, by comap (eᵐ) (completion (twoSidedSat e P)), which is bounded by completion (twoSidedSat e P) by mod-0 shift-invariance of the finite saturation (Oseledets.Krieger.comap_eventuallyMeasurableSpace_twoSidedSat_le). Taking the supremum over m gives the claim. This is the cross-layer analogue of Oseledets.Krieger.twoSidedSat_mono_of_codes.

theorem Oseledets.Krieger.IsGeneratingTwoSidedMod0c.of_codesc {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_3} [Fintype ι] {e : α ≃ᵐ α} (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) {P : Entropy.MeasurePartition μ ι} {Q : κ → Set α} (hQ : IsGeneratingTwoSidedMod0c μ e Q) (hrec : CodesTwoSidedMod0c e Q P) : IsGeneratingTwoSidedMod0 e P

Cross-layer recovery lifts a mod-0 countable two-sided generator to a finite one. If the countable family Q two-sidedly generates (α, e, μ) mod 0 (IsGeneratingTwoSidedMod0c μ e Q) and the two-sided itinerary of the finite partition P recovers each cell of Q mod 0 (CodesTwoSidedMod0c e Q P), then P two-sidedly generates mod 0 in the Fintype sense (Oseledets.Krieger.IsGeneratingTwoSidedMod0 e P).

mα ≤ completion (ctwoSidedSat e Q) (by Q's mod-0 generation) and completion (ctwoSidedSat e Q) ≤ completion (completion (twoSidedSat e P)) ≤ completion (twoSidedSat e P) by cross-layer recovery monotonicity (ctwoSidedSat_mono_of_codesc), completion-monotonicity (Oseledets.Krieger.eventuallyMeasurableSpace_mono), and completion-idempotence (Oseledets.Krieger.eventuallyMeasurableSpace_idem). Chaining gives mα ≤ completion (twoSidedSat e P), i.e. IsGeneratingTwoSidedMod0 e P. This is the cross-layer analogue of Oseledets.Krieger.IsGeneratingTwoSidedMod0.of_codes, bridging the Countable layer (Generator.lean) to the Fintype layer (Coding.lean).

theorem Oseledets.Krieger.CodesTwoSidedMod0c.isGeneratingTwoSidedMod0 {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_3} [Fintype ι] {e : α ≃ᵐ α} (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) {Q : κ → Set α} {P : Entropy.MeasurePartition μ ι} (hQ : IsGeneratingTwoSidedMod0c μ e Q) (hP : CodesTwoSidedMod0c e Q P) : IsGeneratingTwoSidedMod0 e P

A cross-layer mod-0 code of a mod-0 countable two-sided generator is a mod-0 finite two-sided generator — the cross-layer headline reduction. Immediate from IsGeneratingTwoSidedMod0c.of_codesc and the definition of CodesTwoSidedMod0c.

theorem Oseledets.Krieger.codesTwoSidedMod0c_of_aeRecovery {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {ι : Type u_3} [Fintype ι] {e : α ≃ᵐ α} {Q : κ → Set α} {P : Entropy.MeasurePartition μ ι} (hcode : ∀ (j : κ), ∃ (t : Set α), MeasurableSet t ∧ Q j =ᵐ[μ] t) : CodesTwoSidedMod0c e Q P

The convenient sufficient condition for the cross-layer symbolic-code layer (C3). To establish a cross-layer mod-0 code CodesTwoSidedMod0c e Q P of a countable family Q : κ → Set α it suffices to exhibit, for each cell Q j, a twoSidedSat e P-measurable set t with Q j =ᵐ[μ] t — i.e. to recover every Q-cell, up to a μ-null set, from the two-sided P-itinerary of the finite partition P. This is exactly the output of an a.e.-injective measurable block code π : α → (ℤ → Fin k) that recovers the countable Q-name a.e.: each Q-cell is, mod 0, a cylinder event in the P-itinerary, hence twoSidedSat e P-measurable mod 0.

Formally, σ(Q) = generateFrom (range Q), so generateFrom_le reduces the goal to the cells (the range of Q), each handled by the hypothesis. This is the countable analogue of Oseledets.Krieger.codesTwoSidedMod0_of_aeRecovery.

The generation criterion via a standard-Borel generating sequence

The ambient σ-algebra of a standard-Borel space is generated by a fixed countable sequence of measurable sets B = natGeneratingSequence α (Mathlib's generateFrom_natGeneratingSequence, available since StandardBorelSpace α ⇒ MeasurableSpace.CountablyGenerated α). To prove Q two-sidedly generates mod 0, it therefore suffices to recover each Bₘ mod 0 from the two-sided Q-itinerary.

theorem Oseledets.Krieger.isGeneratingTwoSidedMod0c_of_recovers {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α} {Q : κ → Set α} {𝒢 : Set (Set α)} (hgen : MeasurableSpace.generateFrom 𝒢 = mα) (hrec : ∀ s ∈ 𝒢, ∃ (t : Set α), MeasurableSet t ∧ s =ᵐ[μ] t) : IsGeneratingTwoSidedMod0c μ e Q

Two-sided mod-0 generation from per-set recovery. If a countable family of cells Q : κ → Set α recovers every set s of a generating family 𝒢 (generateFrom 𝒢 = mα) up to a μ-null set inside its two-sided saturation ctwoSidedSat e Q, then Q two-sidedly generates mod 0.

The hypothesis says each generator s ∈ 𝒢 is =ᵐ[μ] to a ctwoSidedSat e Q-measurable set, i.e. s ∈ eventuallyMeasurableSpace (ctwoSidedSat e Q) (ae μ); since the completion is a σ-algebra, generateFrom 𝒢 = mα ≤ it.

theorem Oseledets.Krieger.isGeneratingTwoSidedMod0c_of_recovers_natGeneratingSequence {α : Type u_1} {κ : Type u_2} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [StandardBorelSpace α] {e : α ≃ᵐ α} {Q : κ → Set α} (hrec : ∀ (m : ℕ), ∃ (t : Set α), MeasurableSet t ∧ MeasurableSpace.natGeneratingSequence α m =ᵐ[μ] t) : IsGeneratingTwoSidedMod0c μ e Q

Two-sided mod-0 generation from per-natGeneratingSequence recovery (standard-Borel). For a standard-Borel space the ambient σ-algebra is generated by natGeneratingSequence α (generateFrom_natGeneratingSequence). Hence if the ℕ-indexed countable family Q recovers each natGeneratingSequence α m mod 0 inside its two-sided saturation, Q two-sidedly generates mod 0.

This is the convenient generation criterion the Keane–Serafin / Downarowicz limit partition discharges: the inductive construction is steered so that the two-sided itinerary of the limit partition determines membership in every generating set Bₘ off a null set.

The increasing-sequence reduction: generation of the union family

The Keane–Serafin / Downarowicz construction builds an increasing sequence of finite partitions Qₖ, where the level-k partition's two-sided itinerary already recovers the k-th generating set Bₖ mod 0. The union family Q⁺ ⟨k, i⟩ := (Qₖ) i collects all their cells; its generated σ-algebra is the join ⨆ₖ σ(Qₖ) (iSup_generateFrom), so its two-sided saturation contains every comap (eⁿ) σ(Qₖ), hence recovers every Bₖ mod 0 and therefore two-sidedly generates mod 0.

This is the clean structural half of the construction. (The entropy of the union family is not finite — that needs the genuine join atom partition, whose finite static entropy is the supplied summable_index_mass of KeaneSerafinData; the union family only witnesses generation.)

theorem Oseledets.Krieger.generateFrom_sigmaUnion {α : Type u_1} {κ : ℕ → Type u_4} (Q : (k : ℕ) → κ k → Set α) : MeasurableSpace.generateFrom (Set.range fun (p : (k : ℕ) × κ k) => Q p.fst p.snd) = ⨆ (k : ℕ), MeasurableSpace.generateFrom (Set.range (Q k))

The static σ-algebra of the union family Q⁺ ⟨k, i⟩ := Q k i of a countable family of finite-or-countable families Q : ∀ k, κ k → Set α is the supremum ⨆ₖ σ(Q k) of the levels' static σ-algebras.

theorem Oseledets.Krieger.isGeneratingTwoSidedMod0c_sigmaUnion_of_levelRecovers {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [StandardBorelSpace α] {κ : ℕ → Type u_4} {e : α ≃ᵐ α} (Q : (k : ℕ) → κ k → Set α) (hrec : ∀ (m : ℕ), ∃ (t : Set α), MeasurableSet t ∧ MeasurableSpace.natGeneratingSequence α m =ᵐ[μ] t) : IsGeneratingTwoSidedMod0c μ e fun (p : (k : ℕ) × κ k) => Q p.fst p.snd

Generation of the union family from per-level recovery. Suppose, for an increasing sequence of countable families Q : ∀ k, κ k → Set α, that the level-k two-sided saturation recovers the k-th standard-Borel generating set Bₖ mod 0 (each Bₖ =ᵐ[μ] a twoSidedSat cell of the family Q k). Then the union family Q⁺ ⟨k, i⟩ := Q k i two-sidedly generates mod 0.

The proof: ctwoSidedSat e Q⁺ = ⨆ₙ comap (eⁿ) (⨆ₖ σ(Q k)) dominates each level's ctwoSidedSat e (Q k), so a level-k recovery of Bₖ lifts to a Q⁺-recovery; then isGeneratingTwoSidedMod0c_of_recovers_natGeneratingSequence finishes.

The finite-entropy countable two-sided generator: the existence theorem

The Keane–Serafin / Downarowicz construction produces a countable partition Q : ℕ → Set α (the join ⋁ₖ Qₖ of an increasing sequence of finite partitions) with two properties:

• two-sided recovery of the standard-Borel generating sets natGeneratingSequence α mod 0 (so Q two-sidedly generates mod 0); and
• a summable index-mass envelope ∑ i, i·μ(Qᵢ) < ∞, the static finiteness witness produced by the SMB entropy bookkeeping (H(Qₖ) ≤ h(e) + 1, organised so the limit atoms are placed with geometrically decaying index-mass).

The dynamical/analytic content (Rokhlin's lemma + the Shannon–McMillan–Breiman theorem driving the per-step entropy increment) lives entirely in producing this data; it is bundled as KeaneSerafinData. Everything downstream — turning the recovery into mod-0 two-sided generation, and the index-mass envelope into finite static Shannon entropy via Downarowicz's Fact 1.1.4 (cHμ_summable_of_summable_index_mul) — is proved here, unconditionally and sorry-free.

structure Oseledets.Krieger.KeaneSerafinData {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] (μ : MeasureTheory.Measure α) (e : α ≃ᵐ α) : Type u_1

The Keane–Serafin / Downarowicz dynamical input for sub-problem A: the data of a countable partition Q : ℕ → Set α together with the two facts the construction guarantees but whose proof needs the dynamics. Bundling them isolates the open analytic residual (SMB + Rokhlin) from the clean structural reduction.

• cells_measurable: each cell Q i is measurable;
• recovers: each standard-Borel generating set natGeneratingSequence α m is recovered mod 0 by the two-sided Q-itinerary — the generation witness;
• summable_index_mass: the index-weighted total mass ∑ i, i·μ(Qᵢ) is finite — the finite static entropy witness (Downarowicz Fact 1.1.4 input).

• Q : ℕ → Set α

  The countable limit partition Q = ⋁ₖ Qₖ, indexed by ℕ.

• cells_measurable (i : ℕ) : MeasurableSet (self.Q i)

  Each cell of the limit partition is measurable.

• recovers (m : ℕ) : ∃ (t : Set α), MeasurableSet t ∧ MeasurableSpace.natGeneratingSequence α m =ᵐ[μ] t

  The two-sided Q-itinerary recovers each standard-Borel generating set mod 0.

• summable_index_mass : Summable fun (i : ℕ) => ↑i * (μ (self.Q i)).toReal

  The index-weighted total mass ∑ i, i·μ(Qᵢ) is finite (Downarowicz Fact 1.1.4 input).

theorem Oseledets.Krieger.KeaneSerafinData.isGeneratingTwoSidedMod0c {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α} (D : KeaneSerafinData μ e) : IsGeneratingTwoSidedMod0c μ e D.Q

The limit partition of a KeaneSerafinData two-sidedly generates mod 0. Immediate from the recovery witness via isGeneratingTwoSidedMod0c_of_recovers_natGeneratingSequence.

theorem Oseledets.Krieger.KeaneSerafinData.summable_negMulLog {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {e : α ≃ᵐ α} (D : KeaneSerafinData μ e) : Summable fun (i : ℕ) => (μ (D.Q i)).toReal.negMulLog

The limit partition of a KeaneSerafinData has finite static Shannon entropy: the entropy terms i ↦ negMulLog (μ (Qᵢ)).toReal are summable. This is Downarowicz's Fact 1.1.4 (cHμ_summable_of_summable_index_mul) applied to the summable index-mass envelope.

theorem Oseledets.Krieger.exists_countable_twoSided_generator_of_keaneSerafinData {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {e : α ≃ᵐ α} (D : KeaneSerafinData μ e) : ∃ (Q : ℕ → Set α), (∀ (i : ℕ), MeasurableSet (Q i)) ∧ IsGeneratingTwoSidedMod0c μ e Q ∧ Summable fun (i : ℕ) => (μ (Q i)).toReal.negMulLog

The finite-entropy countable two-sided generator (Downarowicz Thm 4.2.3, first half). Given the Keane–Serafin / Downarowicz dynamical data, there is a countable (ℕ-indexed) partition Q that two-sidedly generates (α, e, μ) mod 0 and has finite static Shannon entropy (Summable (fun i => negMulLog (μ (Qᵢ)).toReal), equivalently cHμ μ Q < ∞).

This is sub-problem A of the unconditional Krieger finite generator theorem (issue #15): the static input that is then coded into Fin k by the Rokhlin-tower / name-count combinatorics of Oseledets.Krieger.Coding. The construction of the data D (Rokhlin's lemma + the Shannon–McMillan–Breiman theorem) is the remaining dynamical residual; everything from D to the two conclusions is proved here unconditionally.

theorem Oseledets.Krieger.exists_countable_twoSided_generator {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α} {Q : ℕ → Set α} (hmeas : ∀ (i : ℕ), MeasurableSet (Q i)) (hrec : ∀ (m : ℕ), ∃ (t : Set α), MeasurableSet t ∧ MeasurableSpace.natGeneratingSequence α m =ᵐ[μ] t) (hent : Summable fun (i : ℕ) => (μ (Q i)).toReal.negMulLog) : ∃ (Q : ℕ → Set α), (∀ (i : ℕ), MeasurableSet (Q i)) ∧ IsGeneratingTwoSidedMod0c μ e Q ∧ Summable fun (i : ℕ) => (μ (Q i)).toReal.negMulLog

The finite-entropy countable two-sided generator, from the recovery + entropy data directly. A variant of exists_countable_twoSided_generator_of_keaneSerafinData that takes the two faithful conclusions of sub-problem A as hypotheses on a single countable family Q : ℕ → Set α:

• hrec: the two-sided Q-itinerary recovers each standard-Borel generating set mod 0; and
• hent: the static Shannon entropy is finite (Summable (fun i => negMulLog (μ Qᵢ).toReal)).

The recovers hypothesis is turned into mod-0 two-sided generation by isGeneratingTwoSidedMod0c_of_recovers_natGeneratingSequence. This phrasing keeps the finite static entropy in its weakest faithful form (the entropy summability itself, not the stronger index-mass envelope summable_index_mass), exactly matching the deliverable's target statement.