Shift Invariance of Tail σ-Algebra for Exchangeable Sequences

This file proves that for exchangeable (contractable) sequences, the tail σ-algebra is shift-invariant. Specifically, for contractable sequences:

∫_A f(X_k) dμ = ∫_A f(X_0) dμ

for all k ∈ ℕ and tail-measurable sets A.

Main results

• tailSigma_shift_invariant_for_contractable: The law of the shifted process equals the law of the original process.
• setIntegral_comp_shift_eq: Set integrals over tail-measurable sets are shift-invariant.

Implementation notes

The proofs use the fact that exchangeability implies the measure is invariant under permutations, and the tail σ-algebra "forgets" finite initial segments.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Chapter 1
• Fristedt-Gray (1997), A Modern Approach to Probability Theory, Section II.4

Shift Invariance of Tail σ-Algebra

The key insight: For exchangeable sequences, shifting indices doesn't affect events that depend only on the "tail" of the sequence (events determined by the behavior far out in the sequence).

Mathematically: If X is exchangeable and E ∈ tailSigma X, then: {ω : X₀(ω), X₁(ω), X₂(ω), ... ∈ E} = {ω : X₁(ω), X₂(ω), X₃(ω), ... ∈ E}

This is because permuting the first element doesn't affect tail events.

theorem Exchangeability.Tail.ShiftInvariance.tailSigma_shift_invariant_for_contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) : MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X (1 + i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X i ω) μ

Tail σ-algebra is shift-invariant for exchangeable sequences.

For an exchangeable sequence X, the law of the shifted process equals the law of the original process:

Measure.map (fun ω i => X (1 + i) ω) μ = Measure.map (fun ω i => X i ω) μ

Intuition: Tail events depend only on the behavior "at infinity" - they don't care about the first finitely many coordinates. Exchangeability means we can permute finite initial segments without changing the distribution, so in particular we can "drop" the first element.

theorem Exchangeability.Tail.ShiftInvariance.setIntegral_comp_shift_eq {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (f : α → ℝ) (hf_meas : Measurable f) {A : Set Ω} (hA : MeasurableSet A) (hf_int : MeasureTheory.Integrable (f ∘ X 0) μ) (k : ℕ) : ∫ (ω : Ω) in A, f (X k ω) ∂μ = ∫ (ω : Ω) in A, f (X 0 ω) ∂μ

Key lemma: Set integrals over tail-measurable sets are shift-invariant.

For a contractable sequence X and tail-measurable set A, the integral ∫_A f(X_k) dμ does not depend on k. This follows from the measure-theoretic shift invariance:

• The law of the process (X_0, X_1, ...) on (ℕ → α) is shift-invariant
• Tail-measurable sets correspond to shift-invariant sets in path space
• The integral identity follows from measure invariance