Factorization Lemmas for Martingale Proof

This file contains the conditional independence and factorization lemmas that form the core of the martingale proof of de Finetti's theorem.

Main results

• block_coord_condIndep - Conditional independence of past block and single coordinate given the far future: σ(X₀,...,X_{r-1}) ⊥⊥{σ(θ{m+1} X)} σ(X_r)
• condexp_indicator_inter_of_condIndep - Product formula for conditional expectations under conditional independence
• finite_level_factorization - Finite-level product formula for conditional expectations
• tail_factorization_from_future - Passing finite-level factorization to the tail

These establish that contractability implies the product structure needed for de Finetti's theorem.

theorem Exchangeability.DeFinetti.ViaMartingale.block_coord_condIndep {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m : ℕ} (hrm : r < m) : ProbabilityTheory.CondIndep (futureFiltration X m) (PathSpace.firstRSigma X r) (MeasurableSpace.comap (X r) inferInstance) ⋯ μ

Correct conditional independence from contractability (Kallenberg Lemma 1.3).

For contractable X and r < m, the past block σ(X₀,...,X_{r-1}) and the single coordinate σ(X_r) are conditionally independent given the far future σ(θ_{m+1} X).

Mathematical statement:

σ(X₀,...,X_{r-1}) ⊥⊥_{σ(θ_{m+1} X)} σ(X_r)

Why this is correct: By contractability, deleting coordinate r doesn't change the joint distribution:

(X₀,...,X_{r-1}, θ_{m+1} X) =ᵈ (X₀,...,X_{r-1}, X_r, θ_{m+1} X)

with σ(θ_{m+1} X) ⊆ σ(X_r, θ_{m+1} X).

By Kallenberg's Lemma 1.3: if (U, η) =ᵈ (U, ζ) and σ(η) ⊆ σ(ζ), then U ⊥⊥η ζ. Taking U = (X₀,...,X{r-1}), η = θ_{m+1} X, ζ = (X_r, θ_{m+1} X) gives the result.

This replaces the old broken coordinate_future_condIndep which incorrectly claimed Y ⊥⊥_{σ(Y)} Y.

---

SIMPLIFIED PROOF PATH (using Kallenberg 1.3 infrastructure):

The proof now uses condExp_Xr_indicator_eq_of_contractable which directly applies Kallenberg 1.3 with the true contraction structure:

• W = shiftRV X (m+1) (far future)
• W' = (U, W) where U = firstRMap X r (first r coords)
• Contraction: σ(W) ⊆ σ(U, W) = σ(W')
• Pair law: (X_r, W) =^d (X_r, W') from contractability

This gives: E[1_{X_r ∈ B} | σ(U, W)] = E[1_{X_r ∈ B} | σ(W)] which is the indicator characterization of X_r ⊥⊥ U | W.

The old finite-level approximation approach is now deprecated.

theorem Exchangeability.DeFinetti.ViaMartingale.condexp_indicator_inter_of_condIndep {Ω : Type u_3} {m₀ : MeasurableSpace Ω} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {m mF mH : MeasurableSpace Ω} (hm : m ≤ m₀) (hmF : mF ≤ m₀) (hmH : mH ≤ m₀) (hCI : ProbabilityTheory.CondIndep m mF mH hm μ) {A B : Set Ω} (hA : MeasurableSet A) (hB : MeasurableSet B) : μ[(A ∩ B).indicator fun (x : Ω) => 1|m] =ᵐ[μ] μ[A.indicator fun (x : Ω) => 1|m] * μ[B.indicator fun (x : Ω) => 1|m]

Product formula for conditional expectations under conditional independence.

Given two sets A (measurable in mF) and B (measurable in mH), under conditional independence given m, the conditional expectation of the intersection indicator factors:

μ[1_{A∩B} | m] = μ[1_A | m] · μ[1_B | m]   a.e.

Now proven using condexp_indicator_inter_bridge from CondExp.lean, eliminating the previous : True stub.

theorem Exchangeability.DeFinetti.ViaMartingale.finite_level_factorization {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (r : ℕ) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) (m : ℕ) (hm : m ≥ r) : μ[indProd X r C|futureFiltration X m] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, μ[((C i).indicator fun (x : α) => 1) ∘ X 0|futureFiltration X m] ω

Finite-level factorization builder (formerly Axiom 3).

For a contractable sequence, at any future level m ≥ r, the conditional expectation of the product indicator factors:

μ[∏ᵢ<r 1_{Xᵢ∈Cᵢ} | σ(θₘ₊₁X)] = ∏ᵢ<r μ[1_{X₀∈Cᵢ} | σ(θₘ₊₁X)]

This iteratively applies conditional independence to pull out one coordinate at a time, using contractability to replace each Xᵢ with X₀.

theorem Exchangeability.DeFinetti.ViaMartingale.tail_factorization_from_future {Ω : Type u_3} {α : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) (r : ℕ) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) (h_fact : ∀ m ≥ r, μ[indProd X r C|futureFiltration X m] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, μ[((C i).indicator fun (x : α) => 1) ∘ X 0|futureFiltration X m] ω) (h_rev : ∀ (i : Fin r), ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (m : ℕ) => μ[((C i).indicator fun (x : α) => 1) ∘ X 0|futureFiltration X m] ω) Filter.atTop (nhds (μ[((C i).indicator fun (x : α) => 1) ∘ X 0|tailSigma X] ω))) : μ[indProd X r C|tailSigma X] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, μ[((C i).indicator fun (x : α) => 1) ∘ X 0|tailSigma X] ω

Tail factorization on finite cylinders (formerly Axiom 4).

Assume you have, for all large enough m, the finite‑level factorization at the future filtration:

μ[indProd X r C | σ(θ_{m+1}X)]
  = ∏ i<r μ[1_{X₀∈C i} | σ(θ_{m+1}X)]   a.s.

Then the same factorization holds at the tail σ‑algebra:

μ[indProd X r C | 𝒯_X]
  = ∏ i<r μ[1_{X₀∈C i} | 𝒯_X]           a.s.

This passes the finite‑level equality to the tail using bounded dominated convergence together with reverse martingale convergence.