Tail-level factorization for the de Finetti martingale route #
For a contractable process X, this file factors the conditional expectation of a prefix indicator
product given the tail σ-algebra tailProcess X into a product of single-coordinate tail
conditional expectations — the tail-level input to the de Finetti martingale route.
Main result #
condExp_blockIndicatorProd_tailProcess_ae_eq_prod— for a contractable process, the conditional expectation of the length-rprefix indicator product given the tail σ-algebra factors as the product of the single-coordinate (all replaced byX 0) tail conditional expectations.
Adapted from cameronfreer/exchangeability
(DeFinetti/ViaMartingale/Factorization.lean: tail_factorization_from_future).
theorem
TauCeti.Probability.condExp_blockIndicatorProd_tailProcess_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))
(r : ℕ)
(C : Fin r → Set α)
(hC : ∀ (i : Fin r), MeasurableSet (C i))
:
μ[blockIndicatorProd X (fun (i : Fin r) => ↑i) C | tailProcess X] =ᵐ[μ] fun (ω : Ω) =>
∏ i : Fin r, μ[((C i).indicator fun (x : α) => 1) ∘ X 0 | tailProcess X] ω
Tail-level factorization.
For a contractable process, the conditional expectation of the length-r prefix indicator product
given the tail σ-algebra tailProcess X factors:
μ[∏ i<r 𝟙_{X i ∈ C i} | 𝒯_X] = ∏ i<r μ[𝟙_{X 0 ∈ C i} | 𝒯_X] a.e.