2-sided stationary extension μ_ℤ #

For a stationary process (Ω, T, μ, X) with X : Ω → α (Fintype), this module builds the canonical 2-sided extension μ_ℤ : Measure (ℤ → α) such that:

• the natural ℕ-projection of μ_ℤ agrees with the law of (X ∘ T^[i])_{i ≥ 0},
• the shift σ : (ℤ → α) → (ℤ → α), σ x i := x (i + 1), is μ_ℤ-preserving,
• μ_ℤ is ergodic whenever (Ω, T, μ) is.

The extension is needed because the Shannon–McMillan–Breiman lower bound (liminf blockLogAvg ≥ entropyRate) hinges on the backward Lévy convergence applied to the σ-algebra generated by the negative-time coordinates, which is not available on the one-sided (ℕ-indexed) side. The construction is by Hahn–Kolmogorov extension on the cylinder semiring.

Structure #

The development splits across TwoSidedExtension/Core.lean, TwoSidedExtension/Backward.lean, TwoSidedExtension/PastBlockJointLaw.lean, and TwoSidedExtension/LogCondIntegral.lean:

• shiftedMarginal, the family of finite-dimensional marginals obtained from the one-sided stationary distribution by translating any finite index set into ℕ.
• projective consistency IsProjectiveMeasureFamily + the tendsto_zero σ-additivity input.
• Carathéodory extension μZ via AddContent.measure.
• shift MeasurePreserving + Ergodic transfer.
• coupling (Ω, T, μ) ↔ (ℤ → α, σ, μZ) on the ℕ-projection.
• the forward filtration pastSigma (finite past of length k), forward Lévy upward convergence pmfLogCondPast → pmfLogCondInfty, and the bridge ∫ pmfLogCondInfty dμZ = entropyRate μ p.

Main definitions #

• shiftAmount J — the smallest non-negative offset making every element of J : Finset ℤ non-negative.
• obsZ μ p N J — the joint observation ω ↦ fun j : J ↦ X (T^[(j+N).toNat] ω).
• shiftedMarginal μ p J — μ.map (obsZ μ p (shiftAmount J) J).

Main statements #

• shiftedMarginal_eq_of_shift — N-independence: any sufficient shift gives the same pushforward, via stationarity.
• isProjectiveMeasureFamily_shiftedMarginal — projective consistency.
• instIsProbabilityMeasure_shiftedMarginal — each marginal is a probability measure.