Hewitt–Savage zero–one law

TheoremHewitt–Savage zero–one law#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(S\), and let \(E \subseteq S^{\mathbb{N}}\) be a set that is measurable for the product σ-algebra and invariant under every finitely supported permutation \(\sigma\) of \(\mathbb{N}\), that is, \(\{\omega : \omega \circ \sigma \in E\} = E\) whenever \(\sigma\) moves only finitely many points. Then \(E\) has measure \(0\) or \(1\) under the product measure \(\mu^{\otimes \mathbb{N}}\).

No topological assumption on \(S\) is needed.

theorem hewitt_savage_zero_one_general
    {S : Type*} [MeasurableSpace S]
    (μ : Measure S) [IsProbabilityMeasure μ]
    (E : Set (ℕ → S)) (hE : MeasurableSet E)
    (hSym : ∀ (σ : Equiv.Perm ℕ), Set.Finite {n : ℕ | σ n ≠ n} →
      (fun ω : ℕ → S => ω ∘ ⇑σ) ⁻¹' E = E) :
    Measure.infinitePi (fun _ : ℕ => μ) E = 0 ∨
      Measure.infinitePi (fun _ : ℕ => μ) E = 1

Used by 2

Used byHewitt–Savage zero–one law on a Polish space · Hewitt–Savage zero–one law for i.i.d. sequences

TheoremHewitt–Savage zero–one law on a Polish space#✓fully proved

Let \(S\) be a Polish space with its Borel σ-algebra, let \(\mu\) be a probability measure on \(S\), and let \(E \subseteq S^{\mathbb{N}}\) be a set that is measurable for the product σ-algebra and invariant under every finitely supported permutation \(\sigma\) of \(\mathbb{N}\), that is, \(\{\omega : \omega \circ \sigma \in E\} = E\) whenever \(\sigma\) moves only finitely many points. Then \(E\) has measure \(0\) or \(1\) under the product measure \(\mu^{\otimes \mathbb{N}}\).

The Polish and Borel assumptions are not used in the proof: the same conclusion holds for a probability measure on any measurable space.

@[nolint unusedArguments]
theorem hewitt_savage_zero_one
    {S : Type*} [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S]
    (μ : Measure S) [IsProbabilityMeasure μ]
    (E : Set (ℕ → S)) (hE : MeasurableSet E)
    (hSym : ∀ (σ : Equiv.Perm ℕ), Set.Finite {n : ℕ | σ n ≠ n} →
      (fun ω : ℕ → S => ω ∘ ⇑σ) ⁻¹' E = E) :
    Measure.infinitePi (fun _ : ℕ => μ) E = 0 ∨
      Measure.infinitePi (fun _ : ℕ => μ) E = 1

Sources

• E. Hewitt and L. J. Savage, Symmetric measures on Cartesian products, Trans. Amer. Math. Soc. 80 (1955) 470–501; textbook in Kallenberg, Probabilistic Symmetries and Invariance Principles; general holds for product of identical Borel probabilities.

Uses 1 · Used by 1

Proof usesHewitt–Savage zero–one law

Used byRandom-walk dichotomy on sequence space

DefinitionExchangeable event#✓fully proved

Let \(S\) be a measurable space. A set \(A \subseteq S^{\mathbb{N}}\) is an exchangeable (or permutable) event if it is measurable for the product σ-algebra and \(\{x : x \circ \sigma \in A\} = A\) for every permutation \(\sigma\) of \(\mathbb{N}\) that moves only finitely many indices.

def IsExchangeableEvent {S : Type*} [MeasurableSpace S] (A : Set (ℕ → S)) : Prop :=
  MeasurableSet A ∧
  ∀ σ : Equiv.Perm ℕ, Set.Finite {i | σ i ≠ i} →
    (fun x => x ∘ σ) ⁻¹' A = A

Used by 3

Used byHewitt–Savage zero–one law for i.i.d. sequences · Event exchangeable with respect to a sequence · Exchangeable events of a measurable sequence are measurable

DefinitionEvent exchangeable with respect to a sequence#✓fully proved

Let \(\Omega\) and \(S\) be measurable spaces and let \(X_0, X_1, \ldots : \Omega \to S\) be a sequence of maps. An event \(E \subseteq \Omega\) is exchangeable with respect to \((X_n)\) if there is an exchangeable event \(A \subseteq S^{\mathbb{N}}\) such that \(E = \{\omega \in \Omega : (X_n(\omega))_{n \in \mathbb{N}} \in A\}\).

Equivalently, \(E\) belongs to the σ-field of exchangeable events generated by \((X_n)\).

def IsExchangeableEventWrt {Ω S : Type*} [MeasurableSpace Ω] [MeasurableSpace S]
    (X : ℕ → Ω → S) (E : Set Ω) : Prop :=
  ∃ A : Set (ℕ → S), IsExchangeableEvent A ∧
    E = (fun ω n => X n ω) ⁻¹' A

Uses 1 · Used by 2

Statement usesExchangeable event

Used byHewitt–Savage zero–one law for i.i.d. sequences · Exchangeable events of a measurable sequence are measurable

TheoremExchangeable events of a measurable sequence are measurable#✓fully proved

Let \(\Omega\) and \(S\) be measurable spaces and let \(X_0, X_1, \ldots : \Omega \to S\) be measurable maps. If \(E \subseteq \Omega\) is exchangeable with respect to \((X_n)\), then \(E\) is measurable.

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

Uses 2

Statement usesEvent exchangeable with respect to a sequence

Proof usesExchangeable event

TheoremHewitt–Savage zero–one law for i.i.d. sequences#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(S\) be a measurable space, and let \(X_0, X_1, X_2, \ldots : \Omega \to S\) be measurable maps that are independent under \(\mu\) and each have the same distribution under \(\mu\) as \(X_0\). If an event \(E \subseteq \Omega\) is exchangeable with respect to \((X_n)\), then \(\mu(E) = 0\) or \(\mu(E) = 1\).

theorem hewittSavage_zeroOne
    {Ω S : Type*} [MeasurableSpace Ω] [MeasurableSpace S]
    {μ : Measure Ω} [IsProbabilityMeasure μ]
    {X : ℕ → Ω → S}
    (hX : ∀ n, Measurable (X n))
    (h_ident : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    (h_indep : iIndepFun (m := fun _ => inferInstance) X μ)
    {E : Set Ω}
    (hE : IsExchangeableEventWrt X E) :
    μ E = 0 ∨ μ E = 1

Uses 3

Statement usesEvent exchangeable with respect to a sequence

Proof usesExchangeable event · Hewitt–Savage zero–one law

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.