Kallenberg Chain Lemma for Reverse Filtration

This file implements the core "Kallenberg chain" step from page 28 of Kallenberg (2005).

Main Results

• pair_law_shift_eq_of_contractable - For contractable X with k < m ≤ n: (X k, shiftRV X m) =^d (X k, shiftRV X n)

• condExp_indicator_revFiltration_eq_of_le - The main Kallenberg chain lemma: For contractable X with k < m ≤ n and measurable B: μ[(B.indicator 1) ∘ X k | revFiltration X m] =ᵐ[μ] μ[(B.indicator 1) ∘ X k | revFiltration X n]

Mathematical Background

Kallenberg's argument (page 28):

For a contractable sequence ξ with k < m ≤ n:

P[ξ_k ∈ B | θ_m ξ] = P[ξ_k ∈ B | θ_n ξ]   (a.s.)

where θ_m ξ = (ξ_m, ξ_{m+1}, ...) is the m-shifted sequence.

Proof ingredients:

1. Contractability → pair law: (ξ_k, θ_m ξ) =^d (ξ_k, θ_n ξ) (same strictly increasing subsequence)
2. σ(θ_n ξ) ⊆ σ(θ_m ξ) when m ≤ n (revFiltration_antitone)
3. Kallenberg Lemma 1.3 (condExp_indicator_eq_of_law_eq_of_comap_le)

Notation

In Kallenberg's notation:

• shiftRV X m = θ_m ξ (the m-shifted sequence)
• revFiltration X m = σ(θ_m ξ) (the reverse filtration)
• tailSigma X = T_ξ (the tail σ-algebra)

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, page 28

Pair Law for Shifted Sequences

For contractable X with k < m ≤ n, the pairs (X k, shiftRV X m) and (X k, shiftRV X n) have the same distribution. This follows from contractability by viewing each pair as a strictly increasing subsequence of X.

def Exchangeability.DeFinetti.ViaMartingale.projectPairSeq {α : Type u_2} : (ℕ → α) → α × (ℕ → α)

Equations

• Exchangeability.DeFinetti.ViaMartingale.projectPairSeq f = (f 0, fun (n : ℕ) => f (n + 1))

theorem Exchangeability.DeFinetti.ViaMartingale.projectPairSeq_measurable {α : Type u_2} [MeasurableSpace α] : Measurable projectPairSeq

def Exchangeability.DeFinetti.ViaMartingale.pairInjection (k m : ℕ) : ℕ → ℕ

The injection k, m, m+1, m+2, ... for pair law argument. This is strictly increasing when k < m.

Equations

• Exchangeability.DeFinetti.ViaMartingale.pairInjection k m 0 = k
• Exchangeability.DeFinetti.ViaMartingale.pairInjection k m n.succ = m + n

theorem Exchangeability.DeFinetti.ViaMartingale.pairInjection_strictMono (k m : ℕ) (hk : k < m) : StrictMono (pairInjection k m)

theorem Exchangeability.DeFinetti.ViaMartingale.pair_law_shift_eq_of_contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX : ∀ (n : ℕ), Measurable (X n)) {k m n : ℕ} (hkm : k < m) (hmn : m ≤ n) : MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, shiftRV X m ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, shiftRV X n ω)) μ

Pair law for shifted sequences from contractability.

For contractable X with k < m ≤ n, the pairs (X k, shiftRV X m) and (X k, shiftRV X n) have the same distribution.

Proof: Both pairs correspond to strictly increasing subsequences of X:

• (X k, shiftRV X m) corresponds to indices k, m, m+1, m+2, ...
• (X k, shiftRV X n) corresponds to indices k, n, n+1, n+2, ...

By contractability, these have equal finite marginals, hence equal measures.

Main Kallenberg Chain Lemma

Using the pair law and the contraction structure σ(shiftRV X n) ⊆ σ(shiftRV X m), we apply Kallenberg Lemma 1.3 to drop from revFiltration X m to revFiltration X n.

theorem Exchangeability.DeFinetti.ViaMartingale.condExp_indicator_revFiltration_eq_of_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX : ∀ (n : ℕ), Measurable (X n)) {k m n : ℕ} (hkm : k < m) (hmn : m ≤ n) {B : Set α} (hB : MeasurableSet B) : μ[(X k ⁻¹' B).indicator fun (x : Ω) => 1 | revFiltration X m] =ᵐ[μ] μ[(X k ⁻¹' B).indicator fun (x : Ω) => 1 | revFiltration X n]

Kallenberg Chain Lemma.

For contractable X with k < m ≤ n and measurable B:

μ[(B.indicator 1) ∘ X k | revFiltration X m] =ᵐ[μ] μ[(B.indicator 1) ∘ X k | revFiltration X n]

This is Kallenberg's key observation (page 28): conditioning X_k on the finer σ-algebra σ(θ_n ξ) gives the same result as conditioning on the coarser σ(θ_m ξ).

Proof:

1. (X k, shiftRV X m) =^d (X k, shiftRV X n) by pair_law_shift_eq_of_contractable
2. revFiltration X n ≤ revFiltration X m by revFiltration_antitone
3. Apply Kallenberg Lemma 1.3 (condExp_indicator_eq_of_law_eq_of_comap_le)

Convergence to Tail σ-algebra

Using the Kallenberg chain lemma and reverse martingale convergence, we show that conditional expectations on revFiltration X m equal those on the tail σ-algebra.

theorem Exchangeability.DeFinetti.ViaMartingale.condExp_indicator_revFiltration_eq_tail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX : ∀ (n : ℕ), Measurable (X n)) {k m : ℕ} (hkm : k < m) {B : Set α} (hB : MeasurableSet B) : μ[(X k ⁻¹' B).indicator fun (x : Ω) => 1 | revFiltration X m] =ᵐ[μ] μ[(X k ⁻¹' B).indicator fun (x : Ω) => 1 | tailSigma X]

Conditional expectation on revFiltration equals tail.

For contractable X with k < m, the conditional expectation of the indicator 1_{X_k ∈ B} given revFiltration X m equals the conditional expectation given tailSigma X.

Proof:

1. By condExp_indicator_revFiltration_eq_of_le, the sequence μ[φ | revFiltration X n] is constant for n ≥ m.
2. By condExp_tendsto_iInf, this sequence converges a.e. to μ[φ | tailSigma X].
3. A constant sequence converges to its value, so the value equals the limit.