Conditioning Markov exchangeability on the initial state

Conditioning on a null-measurable initial-state event scales the mass of every finite path starting there and gives zero mass to paths starting elsewhere. Hence it preserves Markov exchangeability. The conditional path-mass formula gives the same mass to paths with the same initial state and transition counts, establishing Markov exchangeability of the conditional law. Null-measurability is all that is asked of the event, so conditioning on a single initial state needs no hypothesis beyond the a.e. measurability that Markov exchangeability already bundles.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115--130.

theorem TauCeti.Probability.prefixLaw_singleton_cond_initial_mem {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {S : Set α} [MeasurableSingletonClass α] (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (hs : MeasureTheory.NullMeasurableSet {ω : Ω | X 0 ω ∈ S} μ) (n : ℕ) (w : Fin (n + 1) → α) : (prefixLaw μ[|{ω : Ω | X 0 ω ∈ S}] X (n + 1)) {w} = (μ {ω : Ω | X 0 ω ∈ S})⁻¹ * if w 0 ∈ S then (prefixLaw μ X (n + 1)) {w} else 0

The mass of a finite path after conditioning on an initial-state event. Paths whose initial state lies outside the conditioning set have zero mass, including when the conditioning event itself has zero mass.

theorem TauCeti.Probability.MarkovExchangeable.cond_initial_mem {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {S : Set α} (h : MarkovExchangeable μ X) (hs : MeasureTheory.NullMeasurableSet {ω : Ω | X 0 ω ∈ S} μ) : MarkovExchangeable μ[|{ω : Ω | X 0 ω ∈ S}] X

Conditioning on a null-measurable initial-state event preserves Markov exchangeability.

theorem TauCeti.Probability.MarkovExchangeable.cond_initial {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {a : α} (h : MarkovExchangeable μ X) : MarkovExchangeable μ[|{ω : Ω | X 0 ω = a}] X

Conditioning on an initial state preserves Markov exchangeability.