def IsExchangeableEvent {S : Type u_2} [MeasurableSpace S] (A : Set (ℕ → S)) : Prop

A set A ⊆ (ℕ → S) is an exchangeable (or permutable) event if it is measurable and invariant under every finite permutation of the index set ℕ, i.e. {x : x ∘ σ ∈ A} = A for every permutation σ that moves only finitely many indices.

def IsExchangeableEventWrt {Ω : Type u_1} {S : Type u_2} [MeasurableSpace S] (X : ℕ → Ω → S) (E : Set Ω) : Prop

An event E ⊆ Ω is exchangeable with respect to the sequence X : ℕ → Ω → S if there is some exchangeable event A ⊆ (ℕ → S) such that E is the pullback of A under ω ↦ (n ↦ X n ω). Equivalently, E belongs to the σ-field of exchangeable events generated by X.

theorem IsExchangeableEventWrt.measurableSet {Ω : Type u_1} {S : Type u_2} [MeasurableSpace Ω] [MeasurableSpace S] {X : ℕ → Ω → S} {E : Set Ω} (hX : ∀ (n : ℕ), Measurable (X n)) (hE : IsExchangeableEventWrt X E) : MeasurableSet E

An exchangeable event with respect to a measurable sequence X is itself measurable in Ω.

theorem hewittSavage_zeroOne {Ω : Type u_3} {S : Type u_4} [MeasurableSpace Ω] [MeasurableSpace S] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → S} (hX : ∀ (n : ℕ), Measurable (X n)) (h_ident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) (h_indep : ProbabilityTheory.iIndepFun X μ) {E : Set Ω} (hE : IsExchangeableEventWrt X E) : μ E = 0 ∨ μ E = 1

Hewitt–Savage 0–1 law. If X_1, X_2, … is an i.i.d. sequence (independent and identically distributed) and E is an exchangeable event (i.e. E ∈ ℰ, the σ-field of permutable events) with respect to X, then μ E ∈ {0, 1}.