The directing measure is the conditional law of every coordinate

directingMeasure_ae_eq_condExp (in DirectingMeasure/Basic.lean) identifies the directing measure with the conditional law of the initial coordinate X 0 given the tail σ-algebra. For a contractable process the same holds for every coordinate. Contractable.directingMeasure_ae_eq_condExp_coord promotes that identity from X 0 to every X m, using the "extreme members agree on the tail" collapse Contractable.condExp_indicator_tailProcess_eq.

This is the per-coordinate input to the de Finetti block-product factorisation: it is what lets the single directing measure serve as the common conditional law of all coordinates.

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/CondExpConvergence.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22).

theorem TauCeti.Probability.Contractable.directingMeasure_ae_eq_condExp_coord {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) (m : ℕ) {B : Set α} (hB : MeasurableSet B) : (fun (ω : Ω) => (directingMeasure μ X ω).real B) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X m | tailProcess X]

The directing measure is the conditional law of every coordinate. For a contractable process and any m, the real evaluation ω ↦ (directingMeasure μ X ω).real B is a version of the conditional expectation of 𝟙_B ∘ X m given the tail σ-algebra tailProcess X.