Basic implications from conditional i.i.d.-ness

A conditionally i.i.d. sequence is exchangeable and contractable, and a conditionally i.i.d. family over any index type is an exchangeable family. These are the easy directions of de Finetti's theorem and of its Ryll-Nardzewski extension to contractable sequences: conditional independence given a directing measure forces every finite selection of coordinates to have the same law, whatever indices are chosen and in whatever order. Each holds both for a named directing measure and in the existential form.

Main results

• ConditionallyIIDWith.exchangeable, ConditionallyIIDWith.contractable — at a named directing measure.
• ConditionallyIID.exchangeable, ConditionallyIID.contractable — their existential corollaries.
• ConditionallyIIDWith.exchangeableFamily, ConditionallyIID.exchangeableFamily — the same implication for families over an arbitrary index type.

theorem TauCeti.Probability.ConditionallyIIDWith.exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : Exchangeable μ X

A sequence with a named directing measure is exchangeable.

theorem TauCeti.Probability.ConditionallyIID.exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : ConditionallyIID μ X) : Exchangeable μ X

A conditionally i.i.d. sequence is exchangeable.

theorem TauCeti.Probability.ConditionallyIIDWith.contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : Contractable μ X

A sequence with a named directing measure is contractable.

theorem TauCeti.Probability.ConditionallyIID.contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : ConditionallyIID μ X) : Contractable μ X

A conditionally i.i.d. sequence is contractable.

theorem TauCeti.Probability.ConditionallyIIDWith.exchangeableFamily {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : ExchangeableFamily μ X

A conditionally i.i.d. family with a named directing measure is exchangeable.

theorem TauCeti.Probability.ConditionallyIID.exchangeableFamily {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) : ExchangeableFamily μ X

A conditionally i.i.d. family is exchangeable.