Future-level factorization for the de Finetti martingale route

For a contractable process X, this file builds the finite-level product factorization of the block-indicator conditional expectation given the future σ-algebra tailFamily X (m+1). Everything is phrased through Mathlib's ProbabilityTheory.CondIndep.

Main results

• condExp_blockIndicatorProd_future_ae_eq_prod — for r ≤ m + 1, the conditional expectation of the length-r prefix indicator product factors as the product of the single-coordinate conditional expectations, with every coordinate replaced by X 0.

The induction is organised through three private helpers: condIndep_prefix_coord_future (prefix/coordinate conditional independence given the future, from Contractable.condIndep_coord_prefix_tail, Kallenberg's Lemma 1.3), condExp_blockCylinder_inter_preimage_ae_eq_mul (the resulting conditional-expectation product split), and condExp_blockIndicatorProd_future_succ (the inductive step).

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/Factorization.lean: block_coord_condIndep, condexp_indicator_inter_of_condIndep, finite_level_factorization).

theorem TauCeti.Probability.condExp_blockIndicatorProd_future_ae_eq_prod {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (m r : ℕ) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) (hm : r ≤ m + 1) : μ[blockIndicatorProd X (fun (i : Fin r) => ↑i) C | tailFamily X (m + 1)] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, μ[((C i).indicator fun (x : α) => 1) ∘ X 0 | tailFamily X (m + 1)] ω

Finite-level future factorization.

For a contractable process and any future level m with r ≤ m + 1, the conditional expectation of the length-r prefix indicator product factors as the product of the single-coordinate conditional expectations, with every coordinate replaced by X 0:

μ[∏ i<r 𝟙_{X i ∈ C i} | tailFamily X (m+1)] = ∏ i<r μ[𝟙_{X 0 ∈ C i} | tailFamily X (m+1)]   a.e.