Shift Invariance of Conditional Expectations for Exchangeable Sequences

This file proves that for exchangeable (contractable) sequences, the conditional expectation of f∘X_n given the tail σ-algebra does not depend on n.

Main results

• condExp_shift_eq_condExp: For a contractable sequence X and integrable function f, μ[f ∘ X n | tail] =ᵐ[μ] μ[f ∘ X 0 | tail] for all n.

Implementation notes

The proof uses the uniqueness characterization of conditional expectation: both sides are tail-measurable, integrable, and have equal set integrals over all tail-measurable sets. The set integral equality follows from setIntegral_comp_shift_eq.

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Theorem 1.2

theorem Exchangeability.Tail.ShiftInvariance.condExp_shift_eq_condExp {Ω : 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) (hf_int : MeasureTheory.Integrable (f ∘ X 0) μ) (n : ℕ) : μ[f ∘ X n|tailProcess X] =ᵐ[μ] μ[f ∘ X 0|tailProcess X]

Shift invariance of conditional expectation for contractable sequences.

For a contractable sequence X and integrable function f, the conditional expectation of f∘X_n given the tail σ-algebra does not depend on n.

This is a standard result in probability theory (see Kallenberg 2005, Theorem 1.2). The proof uses:

• The shifted process (X_n, X_{n+1}, ...) has the same tail σ-algebra as the original
• Conditional expectations are preserved under this identification
• Uses setIntegral_comp_shift_eq as foundation

Note on Cesàro Averages

The lemma cesaro_convergence_all_shifts showing that shifted Cesàro averages (1/m) ∑_{k=0}^{m-1} f(X_{n+k}) converge to μ[f∘X₀ | tailSigma X] for all n ∈ ℕ is implemented in Exchangeability.DeFinetti.ViaL2.CesaroConvergence.

It was moved there to resolve a circular import: that file already imports this one, so the proof (which uses cesaro_to_condexp_L1 from CesaroConvergence) lives there.