InformationTheory.Probability.TwoSidedExtension.Core

The minimal non-negative integer N that makes every element of J non-negative after shifting by N. For empty J we return 0.

For any sufficient shift N, every j ∈ J satisfies 0 ≤ j + N.

The joint observation at ℤ-indexed times, parametrized by a shift N: obsZ μ p N J ω j := X (T^[(j + N).toNat] ω). When N ≥ shiftAmount J, this records the genuine block (X_{j₀+N}, X_{j₁+N}, …) evaluated at the points of J.

The joint observation obsZ μ p N J is measurable.

The finite-dimensional marginal of the (yet-to-be-built) two-sided extension at the index set J : Finset ℤ. Defined as the law of obsZ at the canonical shift shiftAmount J; the value is independent of the chosen shift by stationarity (shiftedMarginal_eq_of_shift).

For two non-negative shifts N₁ ≤ N₂ both valid for J, the joint observation under N₂ is the same as under N₁ precomposed with T^[N₂ - N₁].

N-invariance of obsZ under push-forward (stationarity, single-shift step). For any valid shift N, pushing forward by obsZ μ p (N + k) J agrees with pushing forward by obsZ μ p N J.

N-invariance of the pushforward law (general form): any two valid shifts yield the same pushforward measure.

The shifted marginal coincides with the pushforward of obsZ for any valid shift, not just the canonical shiftAmount J.

Each shifted marginal is a probability measure (pushforward of a probability measure under a measurable map).

Projective consistency: for J ⊆ I, restricting shiftedMarginal μ p I along the inclusion gives shiftedMarginal μ p J.

The AddContent on measurable cylinders of ℤ → α induced by the shifted finite-dimensional marginals.

σ-additivity input: for any antitone sequence of measurable cylinders with empty intersection, the content tends to 0.

The proof uses the finite-type Cantor argument: equipping α with the discrete topology turns ℤ → α into a compact Hausdorff space (Pi.compactSpace from finite discrete factors), every cylinder cylinder I S is closed (preimage of a finite, hence closed, set), and every closed subset of a compact space is compact. Cantor's intersection theorem for sequences (IsCompact.nonempty_iInter_of_sequence_…) then gives ∃ N, A N = ∅, after which stationaryContent (A n) = 0 for n ≥ N.

stationaryContent is σ-subadditive (from tendsto_zero).

The two-sided extension μ_ℤ : Measure (ℤ → α) obtained from the stationary process (Ω, T, μ, X) by Carathéodory extension of the stationaryContent.

On measurable cylinders, μZ agrees with shiftedMarginal.

μZ is the projective limit of the shifted marginals.

μZ is a probability measure.

The two-sided shift σ : (ℤ → α) → (ℤ → α), σ x i := x (i + 1).

The inverse shift, σ⁻¹ x i := x (i - 1).

The shift is measurable.

The inverse shift is measurable.

The two-sided shift preserves μZ.

Proof outline: both μZ μ p and (μZ μ p).map shiftZ are projective limits of the family shiftedMarginal μ p of finite-dimensional marginals. By IsProjectiveLimit.unique they are equal. The projective property of the pushforward reduces to the shift-invariance of the marginals: for any I : Finset ℤ, the marginal at I + 1 (relabeled through the bijection · + 1) equals the marginal at I, which is exactly shiftedMarginal_eq_of_shift.

shiftZSymm is the left-inverse of shiftZ.

shiftZSymm is the right-inverse of shiftZ.

The forward (one-sided) embedding Ω → (ℕ → α), ω ↦ (X (T^[i] ω))_i.

The forward embedding is measurable.

The ℕ-projection of μZ agrees with the law of forwardEmbed.

Both sides are probability measures on ℕ → α. We verify equality on the π-system of measurable cylinders using MeasureTheory.ext_of_generate_finite, then compute each cylinder's measure: on the LHS via μZ_cylinder after rewriting the preimage as a ℤ-cylinder, and on the RHS via the definition of forwardEmbed together with shiftedMarginal_eq_of_shift at shift 0.

Block cylinder under μZ equals the block-law on the one-sided side.

The one-sided (ℕ-indexed) shift σ_ℕ : (ℕ → α) → (ℕ → α), σ_ℕ y i := y (i+1).

The forward shift on ℕ → α is measurable.

The forward embedding semiconjugates T and shiftN.

The ℕ-projection natProj : (ℤ → α) → (ℕ → α), natProj x i := x (i : ℤ).

natProj is measurable.

natProj semiconjugates shiftZ and shiftN.

natProj is measure-preserving from μZ to μ.map forwardEmbed.

forwardEmbed is measure-preserving from μ to its pushforward.

The forward shift on (ℕ → α, μ.map forwardEmbed) is ergodic when the underlying process is ergodic. Direct application of ergodic_of_ergodic_semiconj with forwardEmbed as the measure-preserving semiconjugacy from (Ω, T, μ).

shiftZ iterated k times: shiftZ^[k] x i = x (i + k).

Preimage of a measurable cylinder over F under shiftZ^[k] is a measurable cylinder over F + k = F.image (· + k).

Preimage under shiftZ^[k] preserves measurable cylinders: the preimage of a measurableCylinders element is again in measurableCylinders.

After shifting by k ≥ -F.min (when F is nonempty), the cylinder lies in cylinderEvents {i : ℤ | 0 ≤ i} (the positive-index σ-algebra). The witness index set is F.image (· + k), all of whose elements are ≥ 0.

The positive-index σ-algebra on ℤ → α, i.e., the σ-algebra of events depending only on coordinates i ≥ 0.

posSigma ≤ pi.

natProj is measurable from posSigma to pi on ℕ → α.

A posSigma-measurable set is the natProj-preimage of a measurable set in ℕ → α. This is the factoring lemma: positive-index events factor through natProj.

The two-sided shift is ergodic when the underlying process is ergodic.

By cylinder approximation + ℕ-factor transfer. For any shiftZ-invariant measurable set A, approximate A to within ε by a measurable cylinder, then shift to move the index set into the nonnegative half-line. This yields a posSigma-measurable approximation, so A is μZ-a.e. equal to a posSigma-measurable set A' = natProj⁻¹ B. By ergodicity of shiftN on μ.map forwardEmbed, B is either null or co-null, hence so is A.