Future Rectangles and π-System Machinery

This file contains the π-λ theorem machinery for establishing measure equality on future rectangles B ×ˢ cylinder r C.

Main Results

• contractable_dist_eq_on_first_r_tail - Finite-dimensional cylinder equality
• AgreeOnFutureRectangles - Predicate for measures agreeing on future rectangles
• measure_ext_of_future_rectangles - π-λ extension theorem
• contractable_dist_eq - Full distributional equality from contractability

These are the key lemmas for the reverse martingale proof of de Finetti's theorem.

Finite-Dimensional Cylinder Equality

theorem Exchangeability.DeFinetti.ViaMartingale.contractable_dist_eq_on_first_r_tail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (k m r : ℕ) (hk : k ≤ m) (B : Set α) (hB : MeasurableSet B) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) : μ {ω : Ω | X m ω ∈ B ∧ ∀ (i : Fin r), X (m + (↑i + 1)) ω ∈ C i} = μ {ω : Ω | X k ω ∈ B ∧ ∀ (i : Fin r), X (m + (↑i + 1)) ω ∈ C i}

Finite-dimensional (cylinder) equality: for any r, base set B and measurable sets on the first r tail coordinates, the probabilities agree when comparing (X m, θₘ X) vs (X k, θₘ X).

This is the exact finite-dimensional marginal needed for the martingale step.

Rectangles using future tails and standard cylinders

theorem Exchangeability.DeFinetti.ViaMartingale.preimage_rect_future {Ω : Type u_1} {α : Type u_2} {X : ℕ → Ω → α} (k m r : ℕ) (B : Set α) (C : Fin r → Set α) : have ψ := fun (ω : Ω) => (X k ω, shiftRV X (m + 1) ω); ψ ⁻¹' B ×ˢ PathSpace.cylinder r C = {ω : Ω | X k ω ∈ B ∧ ∀ (i : Fin r), X (m + 1 + ↑i) ω ∈ C i}

Preimage calculation for rectangles with (X k, θ_{m+1}X) and a standard cylinder.

theorem Exchangeability.DeFinetti.ViaMartingale.contractable_dist_eq_on_rectangles_future {Ω : 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) (r : ℕ) (B : Set α) (hB : MeasurableSet B) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) : (MeasureTheory.Measure.map (fun (ω : Ω) => (X m ω, shiftRV X (m + 1) ω)) μ) (B ×ˢ PathSpace.cylinder r C) = (MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, shiftRV X (m + 1) ω)) μ) (B ×ˢ PathSpace.cylinder r C)

Finite-dimensional equality on future rectangles with standard cylinders. For k ≤ m and measurable B, the measures of B × cylinder r C under the pushforwards by ω ↦ (X m ω, θ_{m+1}X(ω)) and ω ↦ (X k ω, θ_{m+1}X(ω)) coincide.

def Exchangeability.DeFinetti.ViaMartingale.AgreeOnFutureRectangles {α : Type u_2} [MeasurableSpace α] (μ ν : MeasureTheory.Measure (α × (ℕ → α))) : Prop

Two measures agree on all future rectangles (sets of form B ×ˢ cylinder r C).

Equations

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

theorem Exchangeability.DeFinetti.ViaMartingale.agree_on_future_rectangles_of_contractable {Ω : 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) : AgreeOnFutureRectangles (MeasureTheory.Measure.map (fun (ω : Ω) => (X m ω, shiftRV X (m + 1) ω)) μ) (MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, shiftRV X (m + 1) ω)) μ)

Measure extension from future rectangles

theorem Exchangeability.DeFinetti.ViaMartingale.measure_ext_of_future_rectangles {α : Type u_2} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (α × (ℕ → α))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (r : ℕ) (B : Set α), MeasurableSet B → ∀ (C : Fin r → Set α), (∀ (i : Fin r), MeasurableSet (C i)) → μ (B ×ˢ PathSpace.cylinder r C) = ν (B ×ˢ PathSpace.cylinder r C)) : μ = ν

theorem Exchangeability.DeFinetti.ViaMartingale.contractable_dist_eq {Ω : 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) : MeasureTheory.Measure.map (fun (ω : Ω) => (X m ω, shiftRV X (m + 1) ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, shiftRV X (m + 1) ω)) μ

Helper lemma: contractability gives the key distributional equality.

If X is contractable, then for any k ≤ m:

(X_m, θ_{m+1} X) =^d (X_k, θ_{m+1} X)

where θ_{m+1} X drops the first coordinate and keeps the future tail ω ↦ (n ↦ X(m + 1 + n) ω).

theorem Exchangeability.DeFinetti.ViaMartingale.AgreeOnFutureRectangles_to_measure_eq {α : Type u_2} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (α × (ℕ → α))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : AgreeOnFutureRectangles μ ν) : μ = ν

Measures that agree on all future rectangles are equal.