de Finetti's Theorem via Reverse Martingales

Aldous' elegant martingale proof of de Finetti's theorem, as presented in Kallenberg (2005) as the "third proof". This approach has medium dependencies.

Status: COMPLETE - 0 sorries in this file. Builds successfully. Remaining sorries are in helper modules (TripleLawDropInfo.lean, CondIndep.lean).

Proof approach

The proof uses a contraction-independence lemma combined with reverse martingale convergence:

1. Lemma 1.3 (Contraction-Independence): If (ξ, η) =^d (ξ, ζ) and σ(η) ⊆ σ(ζ), then ξ ⊥⊥_η ζ.

   Proof idea: For any B, define μ₁ = P[ξ ∈ B | η] and μ₂ = P[ξ ∈ B | ζ]. Then (μ₁, μ₂) is a bounded martingale with μ₁ =^d μ₂, so E(μ₂ - μ₁)² = Eμ₂² - Eμ₁² = 0, implying μ₁ = μ₂ a.s.

2. Main theorem: If ξ is contractable, then ξₙ are conditionally i.i.d. given the tail σ-algebra 𝒯_ξ = ⋂_n σ(θ_n ξ).

From contractability: (ξ_m, θ_{m+1} ξ) =^d (ξ_k, θ_{m+1} ξ) for k ≤ m. Using Lemma 1.3 and reverse martingale convergence:

P[ξ_m ∈ B | θ_{m+1} ξ] = P[ξ_k ∈ B | θ_{m+1} ξ] → P[ξ_k ∈ B | 𝒯_ξ]

This shows conditional independence and identical conditional laws.

Main results

• deFinetti_viaMartingale: Main theorem - contractable implies conditionally i.i.d.
• contraction_independence: Contraction-independence lemma (Kallenberg Lemma 1.3)

Dependencies

⚖️ Medium - Requires martingale theory and reverse martingale convergence ✅ Elegant - Short and conceptually clear proof ✅ Probabilistic - Pure probability theory, no functional analysis

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Lemma 1.3 and page 28: "Third proof of Theorem 1.1"
• Aldous (1983), Exchangeability and related topics

Infrastructure Dependencies

This file is complete (0 sorries). Remaining sorries are in helper modules:

• TripleLawDropInfo.lean (2 sorries) - Kallenberg Lemma 1.3 kernel uniqueness
• CondIndep.lean (5 sorries) - Conditional independence from distributional equality

See VIAMARTINGALE_BLOCKERS.md for detailed status.

Infrastructure for Test Function Transfer (integral_map + Law Equality)

theorem Exchangeability.DeFinetti.ViaMartingale.integral_map_eq {Ω : Type u_1} {δ : Type u_2} [MeasurableSpace Ω] [MeasurableSpace δ] {μ : MeasureTheory.Measure Ω} {T : Ω → δ} (hT : Measurable T) {g : δ → ℝ} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map T μ)) : ∫ (ω : Ω), g (T ω) ∂μ = ∫ (y : δ), g y ∂MeasureTheory.Measure.map T μ

B1: Bochner integral under Measure.map (Change of variables). If T : Ω → δ is measurable and g : δ → ℝ is integrable w.r.t. Measure.map T μ, then ∫ g ∘ T ∂μ = ∫ g ∂ (Measure.map T μ).

This is the Bochner integral analogue of lintegral_map.

theorem Exchangeability.DeFinetti.ViaMartingale.integral_eq_of_map_eq {Ω : Type u_1} {δ : Type u_2} [MeasurableSpace Ω] [MeasurableSpace δ] {μ : MeasureTheory.Measure Ω} {T T' : Ω → δ} (hMeas : Measurable T) (hMeas' : Measurable T') {g : δ → ℝ} (hg : MeasureTheory.Integrable g (MeasureTheory.Measure.map T μ)) (hLaw : MeasureTheory.Measure.map T μ = MeasureTheory.Measure.map T' μ) : ∫ (ω : Ω), g (T ω) ∂μ = ∫ (ω : Ω), g (T' ω) ∂μ

B2: Test-function transfer under equality of laws. If two pushforward measures coincide, Bochner integrals of any integrable function coincide.

theorem Exchangeability.DeFinetti.ViaMartingale.test_fn_pair_law {Ω : Type u_1} {α : Type u_2} {γ : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace γ] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → α) (W W' : Ω → γ) (hY : Measurable Y) (hW : Measurable W) (hW' : Measurable W') (h_pair : MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, W ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (Y ω, W' ω)) μ) (φ : Ω → ℝ) (hφ_factor : ∃ (f : α → ℝ), Measurable f ∧ φ = f ∘ Y) (hφ_int : MeasureTheory.Integrable φ μ) (g : γ → ℝ) (hg : Measurable g) (hg_bdd : ∀ (w : γ), ‖g w‖ ≤ 1) : ∫ (ω : Ω), φ ω * g (W ω) ∂μ = ∫ (ω : Ω), φ ω * g (W' ω) ∂μ

Helper: Generalized test function lemma without ψ factor.

From the pair law (Y,W) =^d (Y,W'), we can swap W and W' for test functions of the form φ(Y) * g(W), where g : γ → ℝ is a bounded measurable function.

This is the key tool for the "swap back" step in the swap-condition-swap technique, where we need to handle functions like φ * (v * 1_B)∘W without the ψ factor.

Proof strategy: Apply the pair law equality directly to the test function F(y,w) = φ(y)*g(w), using integral_map to convert between ∫ F∘(Y,W) and ∫ F d[Law(Y,W)].

Kallenberg Lemma 1.3 (Contraction-Independence): If the triple distribution satisfies (Y, Z, W) =^d (Y, Z, W'), then Y and Z are conditionally independent given W.

This is the key lemma connecting distributional symmetry to conditional independence.

Note: The order (Y, Z, W) matches the natural interpretation where Y is the variable of interest and (Z, W) provides the conditioning information.

Proof strategy: We prove rectangle factorization directly from the distributional equality.

Mathematical content: The distributional equality (Y,Z,W) =^d (Y,Z,W') combined with the implicit "contraction" (W' may contain more information than W) implies that Z provides no additional information about Y beyond what W provides. This is precisely conditional independence.

What's needed to complete: The proof requires showing that for all measurable sets A, B, C with C ∈ σ(W): ∫_C 1_A(Y)·1_B(Z) dμ = (∫_C 1_A(Y)·1_C(W) dμ) · (∫ 1_B(Z)·1_C(W) dμ) / μ(C)

This factorization follows from the distributional equality via a martingale argument (see Kallenberg 2005, proof of Lemma 1.3) or via conditional distributions.

Mathlib target: Mathlib.Probability.ConditionalIndependence.FromDistributionalEquality

theorem Exchangeability.DeFinetti.ViaMartingale.setIntegral_eq_integral_indicator_one_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hs : MeasurableSet s) {f : Ω → ℝ} : ∫ (ω : Ω) in s, f ω ∂μ = ∫ (ω : Ω), s.indicator (fun (x : Ω) => 1) ω * f ω ∂μ

Set integral as 1_s · f (explicit unit indicator), tuned to avoid elaboration blowups.

theorem Exchangeability.DeFinetti.ViaMartingale.ae_bound_condexp_of_ae_bound {Ω : Type u_1} [m0 : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {m : MeasurableSpace Ω} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] {g : Ω → ℝ} {C : ℝ} (hgC : ∀ᵐ (ω : Ω) ∂μ, |g ω| ≤ C) : ∀ᵐ (ω : Ω) ∂μ, |μ[g|m] ω| ≤ C

If |g| ≤ C a.e., then |μ[g|m]| ≤ C a.e. (uses monotonicity of conditional expectation).

theorem Exchangeability.DeFinetti.ViaMartingale.integral_mul_condexp_adjoint_Linfty {Ω : Type u_1} [m0 : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {m : MeasurableSpace Ω} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] {g ξ : Ω → ℝ} {C : ℝ} (hgC : ∀ᵐ (ω : Ω) ∂μ, |g ω| ≤ C) (hg : MeasureTheory.Integrable g μ) (hξ : MeasureTheory.Integrable ξ μ) : ∫ (ω : Ω), g ω * μ[ξ|m] ω ∂μ = ∫ (ω : Ω), μ[g|m] ω * ξ ω ∂μ

Adjointness for bounded g (L∞–L¹): If g is essentially bounded and ξ ∈ L¹(μ), then ∫ g · μ[ξ|m] = ∫ μ[g|m] · ξ.

This avoids the L¹×L¹ product pitfall by using L∞ control on g, and the corresponding L∞ control on μ[g|m].

theorem Exchangeability.DeFinetti.ViaMartingale.indicator_comp_preimage_one {Ω : Type u_1} {S : Type u_2} [MeasurableSpace S] {W : Ω → S} {T : Set S} : (fun (ω : Ω) => T.indicator (fun (x : S) => 1) (W ω)) = (W ⁻¹' T).indicator fun (x : Ω) => 1

theorem Exchangeability.DeFinetti.ViaMartingale.integral_mul_indicator_to_set {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {S : Set Ω} (hS : MeasurableSet S) (f : Ω → ℝ) : ∫ (ω : Ω), f ω * S.indicator (fun (x : Ω) => 1) ω ∂μ = ∫ (ω : Ω) in S, f ω ∂μ

Main Theorem: de Finetti via Reverse Martingales

theorem Exchangeability.DeFinetti.ViaMartingale.finite_product_formula_with_directing {Ω : Type u_5} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {α : Type u_6} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (m : ℕ) (k : Fin m → ℕ) (hk : StrictMono k) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin m) => X (k i) ω) μ = μ.bind fun (ω : Ω) => MeasureTheory.Measure.pi fun (x : Fin m) => directingMeasure X hX_meas ω

Mixture representation on every finite block (strict‑mono version) using the canonical directing measure.

This is the key infrastructure lemma that assembles all the pieces:

• directingMeasure with its probability and measurability properties
• conditional_law_eq_directingMeasure extending X₀-marginal to all coordinates
• finite_product_formula for the strict-mono product identity

The public-facing theorem deFinetti_viaMartingale is in TheoremViaMartingale.lean.

Notes

The main de Finetti theorem using this machinery is in TheoremViaMartingale.lean. This file provides the proof infrastructure (helper lemmas and constructions).