Recovering a directing measure from an infinite subsequence

Every infinite injective selection from a conditionally i.i.d. family determines its directing measure almost surely. More precisely, the directing measure is almost surely a measurable function of the selected path. This lets an infinite hidden part of an exchangeable family supply the directing measure for the whole family, including its visible coordinates.

We apply de Finetti on the selected path space and use uniqueness of the joint law of a directing measure and its process. This works for finite base measures and a.e.-measurable coordinates, without a standard Borel assumption on the sample space.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, §1.1.

theorem TauCeti.Probability.ConditionallyIIDWith.exists_measurable_directing_eq_comp {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {k : ℕ → ι} (hk : Function.Injective k) : ∃ (F : (ℕ → α) → MeasureTheory.ProbabilityMeasure α), Measurable F ∧ ν =ᵐ[μ] fun (ω : Ω) => F fun (n : ℕ) => X (k n) ω

A directing measure is almost surely a measurable function of any infinite injective selection of the process. The selection need not preserve an order, and the original family may have an arbitrary index type.