Shift-invariant σ-algebra on path space

This file defines the shift-invariant σ-algebra on path space and establishes basic measurability properties.

Main definitions

• tailSigma: The tail σ-algebra generated by the iterates of the left shift.
• isShiftInvariant: Predicate for sets that are invariant under the shift map.
• shiftInvariantSigma: The σ-algebra of shift-invariant sets.

Main results

• isShiftInvariant_iff: Characterization of shift-invariance in terms of membership.
• shiftInvariantSigma_le: The shift-invariant σ-algebra is a sub-σ-algebra.
• mem_shiftInvariantSigma_iff: Membership in the invariant σ-algebra.
• shiftInvariantSigma_measurable_shift_eq: Shift-invariant measurability forces pointwise invariance under the shift map.

References

• Olav Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Springer, Chapter 1 (pages 26-27). The shift-invariant σ-algebra is denoted 𝓘_ξ in Kallenberg.
• FMP 10.4: Invariant sets and functions (Chapter 10, pages 180-181).

def Exchangeability.DeFinetti.tailSigma {α : Type u_1} [MeasurableSpace α] : MeasurableSpace Ω[α]

The tail σ-algebra generated by the iterates of the left shift on path space.

Equations

• Exchangeability.DeFinetti.tailSigma = ⨅ (n : ℕ), MeasurableSpace.comap (fun (ω : Ω[α]) => Exchangeability.PathSpace.shift^[n] ω) inferInstance

def Exchangeability.DeFinetti.isShiftInvariant {α : Type u_1} [MeasurableSpace α] (s : Set Ω[α]) : Prop

A set is shift-invariant if it is measurable and equals its preimage under shift.

Equations

• Exchangeability.DeFinetti.isShiftInvariant s = (MeasurableSet s ∧ Exchangeability.PathSpace.shift ⁻¹' s = s)

theorem Exchangeability.DeFinetti.isShiftInvariant_iff {α : Type u_1} [MeasurableSpace α] {s : Set Ω[α]} : isShiftInvariant s ↔ MeasurableSet s ∧ ∀ (ω : ℕ → α), PathSpace.shift ω ∈ s ↔ ω ∈ s

def Exchangeability.DeFinetti.shiftInvariantSigma {α : Type u_1} [MeasurableSpace α] : MeasurableSpace Ω[α]

The shift-invariant σ-algebra: the collection of shift-invariant sets.

This is defined directly as the sub-σ-algebra of measurable shift-invariant sets.

Equations

• One or more equations did not get rendered due to their size.

theorem Exchangeability.DeFinetti.shiftInvariantSigma_le {α : Type u_1} [MeasurableSpace α] : shiftInvariantSigma ≤ inferInstance

theorem Exchangeability.DeFinetti.mem_shiftInvariantSigma_iff {α : Type u_1} [MeasurableSpace α] {s : Set Ω[α]} : MeasurableSet s ↔ isShiftInvariant s

theorem Exchangeability.DeFinetti.shiftInvariantSigma_measurable_shift_eq {α : Type u_1} [MeasurableSpace α] (g : Ω[α] → ℝ) (hg : Measurable g) : (fun (ω : ℕ → α) => g (PathSpace.shift ω)) = g

Shift-invariant measurability forces pointwise invariance under the shift map.

theorem Exchangeability.DeFinetti.shift_iterate_measurable {α : Type u_1} [MeasurableSpace α] (n : ℕ) : Measurable PathSpace.shift^[n]

theorem Exchangeability.DeFinetti.shiftInvariant_implies_shiftInvariantMeasurable {α : Type u_1} [MeasurableSpace α] (g : Ω[α] → ℝ) (hg : Measurable g) (hinv : ∀ (ω : ℕ → α), g (PathSpace.shift ω) = g ω) : Measurable g

A function that is pointwise shift-invariant and measurable is measurable with respect to the shift-invariant σ-algebra.