De Finetti's theorem for countable index types

De Finetti's theorem is independent of the particular enumeration of a countably infinite index type. This file transports the sequence theorem along an equivalence with ℕ.

Main results

• conditionallyIID_of_exchangeableFamily_of_equiv_nat gives the transport along an explicit equivalence ι ≃ ℕ.
• conditionallyIID_of_exchangeableFamily chooses such an equivalence from [Countable ι] and [Infinite ι].

This implements the Layer 8 target “de Finetti for other countable index types” in TauCetiRoadmap/Exchangeability/README.md. The proof reuses the sequence theorem conditionallyIID_of_exchangeable; no new measure-theoretic argument is required.

theorem TauCeti.Probability.conditionallyIID_of_exchangeableFamily_of_equiv_nat {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} (hX : ExchangeableFamily μ X) (e : ι ≃ ℕ) (hX_meas : ∀ (i : ι), Measurable (X i)) : ConditionallyIID μ X

De Finetti's theorem transported along an explicit enumeration. Under a finite measure, an exchangeable family with measurable coordinates whose index type is equivalent to ℕ is conditionally i.i.d.

theorem TauCeti.Probability.conditionallyIID_of_exchangeableFamily {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] [Infinite ι] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} (hX : ExchangeableFamily μ X) (hX_meas : ∀ (i : ι), Measurable (X i)) : ConditionallyIID μ X

De Finetti's theorem for countably infinite index types. Under a finite measure, every exchangeable family with measurable coordinates indexed by a countably infinite type, with values in a nonempty standard Borel space, is conditionally i.i.d.