Bridge: directing_measure is the pushforward of condExpKernel by X 0

directing_measure X … ω is, almost everywhere in ω, the pushforward of the conditional-expectation kernel condExpKernel μ (tailSigma X) ω by the first coordinate X 0. This identifies the directing measure as the conditional distribution of X 0 given the tail σ-algebra and lets downstream integration identities follow from mathlib's kernel API. Added in isolation; downstream migrations land in a follow-up PR.

theorem Exchangeability.DeFinetti.ViaL2.directing_measure_ae_eq_condExpKernel_map {Ω : Type u_1} [MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX_contract : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) (hX_L2 : ∀ (i : ℕ), MeasureTheory.MemLp (X i) 2 μ) : (fun (ω : Ω) => directing_measure X hX_contract hX_meas hX_L2 ω) =ᵐ[μ] fun (ω : Ω) => MeasureTheory.Measure.map (X 0) ((ProbabilityTheory.condExpKernel μ (Tail.tailProcess X)) ω)

The bridge identifying directing_measure ω with the pushforward of condExpKernel μ (tailSigma X) ω by X 0.