Shift-invariant representatives via limsup construction

This file constructs canonical shift-invariant representatives for functions that are almost shift-invariant (i.e., g ∘ shift = g a.e.).

Main definitions

• gRep: Canonical shift-invariant representative via limsup along the orbit.
• mkShiftInvariantRep: Given an a.e. shift-invariant function, construct a representative that is literally shift-invariant and measurable with respect to shiftInvariantSigma.
• exists_shiftInvariantRepresentative: Existence theorem for shift-invariant representatives.

Main results

• gRep_measurable: The limsup representative is measurable.
• gRep_shiftInvariant: The limsup representative is pointwise shift-invariant.
• gRep_ae_eq_of_constant_orbit: The representative agrees with the original a.e.
• exists_shiftInvariantFullMeasureSet: Construction of shift-invariant full-measure sets.

Mathematical idea

For each ω, consider the orbit sequence g0(ω), g0(shift ω), g0(shift² ω), .... If g0 is almost invariant, then this sequence is eventually constant on a full-measure set. Taking the limsup gives a well-defined function that is:

1. Shift-invariant: gRep g0 (shift ω) = gRep g0 ω for all ω (not just a.e.)
2. Measurable: Inherits measurability from g0
3. Almost equal: gRep g0 =ᵐ[μ] g0 when g0 is almost invariant

This construction avoids the Axiom of Choice by using a canonical limit process rather than selecting arbitrary representatives from equivalence classes.

References

• Olav Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Springer, Chapter 1.

Limsup construction for shift-invariant representatives

Given a function g0 : Ω[α] → ℝ that is almost shift-invariant (i.e., g0 ∘ shift = g0 a.e.), we construct a pointwise shift-invariant representative gRep g0 using a limsup along the orbit.

Key property: If g0 (shift^[n] ω) = g0 ω for all n, then gRep g0 ω = g0 ω.

def Exchangeability.DeFinetti.gRep {α : Type u_1} (g0 : Ω[α] → ℝ) : Ω[α] → ℝ

Canonical shift-invariant representative via limsup.

Given g0 : Ω[α] → ℝ, this constructs a shift-invariant function gRep g0 by taking the limsup along the shift orbit and converting back to ℝ.

Properties:

• If g0 is measurable, so is gRep g0 (see gRep_measurable)
• gRep g0 (shift ω) = gRep g0 ω for all ω (see gRep_shiftInvariant)
• If g0 (shift^[n] ω) = g0 ω for all n, then gRep g0 ω = g0 ω (see gRep_eq_of_constant_orbit)
• If g0 ∘ shift =ᵐ[μ] g0, then gRep g0 =ᵐ[μ] g0 (see gRep_ae_eq_of_constant_orbit)

Equations

• Exchangeability.DeFinetti.gRep g0 ω = (Exchangeability.DeFinetti.gLimsupE✝ g0 ω).toReal

theorem Exchangeability.DeFinetti.gRep_measurable {α : Type u_1} [MeasurableSpace α] {g0 : Ω[α] → ℝ} (hg0 : Measurable g0) : Measurable (gRep g0)

theorem Exchangeability.DeFinetti.gRep_shiftInvariant {α : Type u_1} {g0 : Ω[α] → ℝ} (ω : ℕ → α) : gRep g0 (PathSpace.shift ω) = gRep g0 ω

theorem Exchangeability.DeFinetti.gRep_eq_of_constant_orbit {α : Type u_1} {g0 : Ω[α] → ℝ} {ω : Ω[α]} (hconst : ∀ (n : ℕ), g0 (PathSpace.shift^[n] ω) = g0 ω) : gRep g0 ω = g0 ω

theorem Exchangeability.DeFinetti.gRep_ae_eq_of_constant_orbit {α : Type u_1} [MeasurableSpace α] {g0 : Ω[α] → ℝ} {μ : MeasureTheory.Measure Ω[α]} (hconst : ∀ᵐ (ω : ℕ → α) ∂μ, ∀ (n : ℕ), g0 (PathSpace.shift^[n] ω) = g0 ω) : gRep g0 =ᵐ[μ] g0

theorem Exchangeability.DeFinetti.ae_shift_invariance_on_rep {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) {f g : Ω[α] → ℝ} (hfg : g =ᵐ[μ] f) (hshift : (fun (ω : Ω[α]) => f (PathSpace.shift ω)) =ᵐ[μ] f) : (fun (ω : Ω[α]) => g (PathSpace.shift ω)) =ᵐ[μ] g

Construction of shift-invariant representatives

The main challenge in working with shift-invariant functions is that almost-everywhere equality g ∘ shift =ᵐ[μ] g doesn't immediately give a pointwise invariant function.

Goal: Given g : Ω[α] → ℝ with g ∘ shift =ᵐ[μ] g, construct g' : Ω[α] → ℝ such that:

1. g' (shift ω) = g' ω for ALL ω (pointwise, not just a.e.)
2. g' =ᵐ[μ] g (almost equal to the original)
3. g' is measurable with respect to shiftInvariantSigma

Strategy:

1. Find a shift-invariant full-measure set S where g is constant along orbits
2. Use gRep to construct a pointwise invariant representative
3. Prove the representative agrees with g almost everywhere

This avoids Choice by using the canonical gRep construction instead of selecting arbitrary representatives.

theorem Exchangeability.DeFinetti.mkShiftInvariantRep {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (g : Ω[α] → ℝ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hshift : (fun (ω : Ω[α]) => g (PathSpace.shift ω)) =ᵐ[μ] g) : ∃ (g' : Ω[α] → ℝ), MeasureTheory.AEStronglyMeasurable g' μ ∧ (∀ᵐ (ω : Ω[α]) ∂μ, g' ω = g ω) ∧ ∀ (ω : ℕ → α), g' (PathSpace.shift ω) = g' ω

Given an AEStronglyMeasurable function whose shift agrees with it almost everywhere, construct a representative that is literally shift-invariant and measurable with respect to the invariant σ-algebra.

theorem Exchangeability.DeFinetti.exists_shiftInvariantRepresentative {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (g : Ω[α] → ℝ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hinv : (fun (ω : Ω[α]) => g (PathSpace.shift ω)) =ᵐ[μ] g) : ∃ (g' : Ω[α] → ℝ), MeasureTheory.AEStronglyMeasurable g' μ ∧ (∀ᵐ (ω : Ω[α]) ∂μ, g' ω = g ω) ∧ ∀ (ω : ℕ → α), g' (PathSpace.shift ω) = g' ω

Main construction: given a function that agrees with its shift a.e., produce a shift-invariant representative.