Conditional Expectation Convergence from Contractability

This file proves that for contractable processes, conditional expectations of indicators converge to the tail conditional expectation.

Main results

• condexp_convergence - For k ≤ m, P[X_m ∈ B | θ_{m+1} X] = P[X_k ∈ B | θ_{m+1} X]
• extreme_members_equal_on_tail - P[X_m ∈ B | tail] = P[X_0 ∈ B | tail]

These are key steps in the martingale proof of de Finetti's theorem.

Conditional expectation convergence from contractability

theorem Exchangeability.DeFinetti.ViaMartingale.condexp_convergence {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (k m : ℕ) (hk : k ≤ m) (B : Set α) (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X m|futureFiltration X m] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X k|futureFiltration X m]

Conditional expectation convergence: For k ≤ m, all coordinates look the same when conditioned on the future filtration at level m.

This is the key convergence result: for k ≤ m and measurable set B,

P[X_m ∈ B | θ_{m+1} X] = P[X_k ∈ B | θ_{m+1} X]

Proof: Uses the CE bridge lemma from CondExp.lean with the measure equality from contractability. The key insight is that deleting coordinates doesn't change the joint distribution with the future, which implies conditional expectation equality by the bridge lemma.

theorem Exchangeability.DeFinetti.ViaMartingale.extreme_members_equal_on_tail_via_tower {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (m : ℕ) (B : Set α) (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X m|tailSigma X] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X 0|tailSigma X]

Conditional expectations of indicators are equal on the tail σ-algebra (tower proof).

For any contractable process X and measurable set B,

P[X_m ∈ B | tail] = P[X_0 ∈ B | tail]

Proof: Uses condexp_convergence at level m, then applies tower property since tailSigma ≤ futureFiltration m.

This is an alternative proof using the tower property. See extreme_members_equal_on_tail for the Kallenberg-style proof using reverse martingale convergence.

theorem Exchangeability.DeFinetti.ViaMartingale.extreme_members_equal_on_tail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (m : ℕ) (B : Set α) (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X m|tailSigma X] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X 0|tailSigma X]

Conditional expectations of indicators are equal on the tail σ-algebra.

For any contractable process X and measurable set B,

P[X_m ∈ B | tail] = P[X_0 ∈ B | tail]

Proof (Kallenberg route):

1. By condExp_indicator_revFiltration_eq_tail, conditioning on revFiltration X (m+1) equals conditioning on tailSigma X (via reverse martingale convergence).
2. By condexp_convergence, both indicators have equal conditional expectation given futureFiltration X m = revFiltration X (m+1).
3. Combine to get equality on the tail.

This is the Kallenberg-style proof using the chain lemma and reverse martingale convergence. See extreme_members_equal_on_tail_via_tower for an alternative proof using the tower property.

@[reducible, inline]

abbrev Exchangeability.DeFinetti.ViaMartingale.𝔽 {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] {X : ℕ → Ω → α} (m : ℕ) : MeasurableSpace Ω

𝔽ₘ := σ(θ_{m+1} X) (the future filtration).

Equations

• Exchangeability.DeFinetti.ViaMartingale.𝔽 m = Exchangeability.DeFinetti.ViaMartingale.futureFiltration X m

theorem Exchangeability.DeFinetti.ViaMartingale.filtration_antitone {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) : Antitone fun (m : ℕ) => futureFiltration X m

The reverse filtration is decreasing; packaged for the martingale API.

noncomputable def Exchangeability.DeFinetti.ViaMartingale.M {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (k : ℕ) (B : Set α) (_hB : MeasurableSet B) : ℕ → Ω → ℝ

Mₘ := 𝔼[1_{Xₖ∈B} | 𝔽ₘ]. The reverse martingale sequence for the indicator of X_k in B.

Uses condExpWith from CondExp.lean to manage typeclass instances properly.

Equations

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