The two-sided coordinate partition is two-sided generating (literal, not mod-0)

The Krieger finite-generator interface (Oseledets/Krieger/ZIterate.lean) consumes a two-sided generating partition: IsGeneratingTwoSided e P asserts that the smallest ziter e-pullback-stable σ-algebra containing σ(P) saturates the whole product σ-algebra, ⨆ n : ℤ, comap (ziter e n) σ(P) = mα.

This file discharges that hypothesis literally (not merely modulo 0) for the canonical setup: the invertible left shift biShiftEquiv on the two-sided full shift BiShift α₀ := ℤ → α₀ with the time-0 coordinate partition coordPartitionZFin and any (Bernoulli) measure bernZ ν. The statement is true on the nose — no measure-theoretic approximation is needed — because the two-sided shift exactly translates coordinate σ-algebras and the product σ-algebra over ℤ is, by definition, the supremum of all coordinate comaps.

The argument (porting the one-sided coordPartition_isGenerating to ℤ)

• σ(coordPartitionZ) is the time-0 coordinate σ-algebra. The cells {x | x 0 = i} are exactly the singleton preimages of the 0-th projection; over a finite alphabet a measurable subset of α₀ is a finite union of singletons, so generatedSigmaAlgebra (coordPartitionZ) = coordSigmaZ 0 (generatedSigmaAlgebra_coordPartitionZ_eq). The Fin-reindexed partition coordPartitionZFin generates the same σ-algebra (reindexing leaves the range of cells unchanged, generatedSigmaAlgebra_coordPartitionZFin_eq).
• ziter biShiftEquiv n translates coordinates. ziter biShiftEquiv n x i = x (i + n) (ziter_biShiftEquiv_apply), so eval 0 ∘ ziter biShiftEquiv n = eval n and hence comap (ziter biShiftEquiv n) (coordSigmaZ 0) = coordSigmaZ n (comap_ziter_coordSigmaZ).
• The ℤ-supremum is the full σ-algebra. Every integer coordinate n is hit, so ⨆ n : ℤ, coordSigmaZ n = MeasurableSpace.pi = mα (pi_eq_iSup_coordSigmaZ).

Main result

• Oseledets.Multifractal.coordPartitionZFin_isGeneratingTwoSided: IsGeneratingTwoSided biShiftEquiv (coordPartitionZFin (bernZ ν)).

σ(coordPartitionZ) is the time-0 coordinate σ-algebra

theorem Oseledets.Multifractal.generatedSigmaAlgebra_coordPartitionZ_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (μ : MeasureTheory.Measure (BiShift α₀)) : Entropy.generatedSigmaAlgebra μ (coordPartitionZ μ) = coordSigmaZ 0

The σ-algebra generated by the two-sided coordinate partition is the 0-th coordinate σ-algebra coordSigmaZ 0 = comap (eval 0) m: the cells {x | x 0 = i} are exactly the singleton preimages of the 0-th projection, and over a finite alphabet a measurable subset of α₀ is a finite union of singletons, so the two generated σ-algebras coincide. (Two-sided port of generatedSigmaAlgebra_coordPartition_eq.)

theorem Oseledets.Multifractal.generatedSigmaAlgebra_coordPartitionZFin_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (μ : MeasureTheory.Measure (BiShift α₀)) : Entropy.generatedSigmaAlgebra μ (coordPartitionZFin μ) = Entropy.generatedSigmaAlgebra μ (coordPartitionZ μ)

The σ-algebra generated by the Fin-reindexed two-sided coordinate partition equals that of the original: a bijective reindexing leaves the range of cells unchanged. (Two-sided port of generatedSigmaAlgebra_coordPartitionFin_eq.)

ziter biShiftEquiv n translates coordinates

theorem Oseledets.Multifractal.biShiftEquiv_symm_iterate_apply {α₀ : Type u_1} [MeasurableSpace α₀] (m : ℕ) (x : BiShift α₀) (i : ℤ) : (⇑biShiftEquiv.symm)^[m] x i = x (i - ↑m)

The m-th forward iterate of the inverse shift retreats every (integer) index by m: (biShiftEquiv.symm)^[m] x i = x (i - m).

theorem Oseledets.Multifractal.ziter_biShiftEquiv_apply {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℤ) (x : BiShift α₀) (i : ℤ) : Krieger.ziter biShiftEquiv n x i = x (i + n)

The two-sided iterate translates coordinates. The two-sided iterate ziter biShiftEquiv n advances every (integer) index by n: ziter biShiftEquiv n x i = x (i + n). For n ≥ 0 this is the forward-shift iterate formula biShiftMap^[k] x i = x (i + k); for n < 0 it is the inverse-shift iterate formula biShiftEquiv_symm_iterate_apply.

theorem Oseledets.Multifractal.comap_ziter_coordSigmaZ {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℤ) : MeasurableSpace.comap (Krieger.ziter biShiftEquiv n) (coordSigmaZ 0) = coordSigmaZ n

Per-n pullback identity. Pulling back the time-0 coordinate σ-algebra along the two-sided iterate ziter biShiftEquiv n gives the n-th coordinate σ-algebra: comap (ziter biShiftEquiv n) (coordSigmaZ 0) = coordSigmaZ n. Indeed eval 0 ∘ ziter biShiftEquiv n = eval n since ziter biShiftEquiv n x 0 = x n.

The two-sided generating property

theorem Oseledets.Multifractal.coordPartitionZFin_isGeneratingTwoSided {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Krieger.IsGeneratingTwoSided biShiftEquiv (coordPartitionZFin (bernZ ν))

The two-sided coordinate partition is two-sided generating. For the invertible left shift biShiftEquiv on the two-sided full shift BiShift α₀ with the two-sided i.i.d. (Bernoulli) measure bernZ ν, the Fin-reindexed time-0 coordinate partition coordPartitionZFin is two-sided generating in the literal (not merely mod-0) sense of Krieger's interface: ⨆ n : ℤ, comap (ziter biShiftEquiv n) σ(coordPartitionZFin) = mα.

The reindexed partition generates the same σ-algebra as coordPartitionZ, namely the time-0 coordinate σ-algebra coordSigmaZ 0; the two-sided iterate at n pulls this back to the n-th coordinate σ-algebra coordSigmaZ n; and the product σ-algebra over ℤ is, by definition, the supremum of all the coordinate σ-algebras, so the ℤ-saturation recovers mα.