The Hewitt–Savage zero-one law

For an i.i.d. sequence, the exchangeable (symmetric) σ-algebra on path space is trivial: every exchangeable event has probability 0 or 1 (hewittSavage_trivial_of_iIndep).

Kolmogorov's tail zero-one law does not subsume this. Tail triviality needs only independence, whereas the symmetric σ-algebra can contain events that are not tail events: for a measurable B with B ≠ ∅ and B ≠ Set.univ, the event {p | ∃ n, p n ∈ B} is invariant under every permutation of the coordinates, yet is not a tail event — some path witnesses it only at index 0, and changing that one coordinate moves the path out of the event, whereas tail events are invariant under modification of finitely many coordinates. The qualification matters: for B = ∅ or B = Set.univ, or a one-point coordinate space, the event collapses to ∅ or Set.univ and is a tail event after all.

pathTail_le_exchangeableSigma records the inclusion of the two σ-algebras formally; its strictness is not formalized here.

Identical distribution enters only as the route to exchangeability of the path law: it is what Exchangeable.of_iIndepFun_identDistrib consumes, and exchangeability is what the argument below actually uses. It is sufficient for that, not necessary for the conclusion — the abstract form measure_eq_zero_or_one_of_exchangeableSigma assumes an exchangeable law and the disjoint-block product formula directly, and mentions identical distribution nowhere. A deterministic independent sequence with distinct constant coordinates, for instance, is not identically distributed yet has a Dirac path law, under which every event is trivial.

Main results

• hewittSavage_trivial_of_iIndep — the zero-one law, from iIndepFun and IdentDistrib.
• measure_eq_zero_or_one_of_exchangeableSigma — the abstract form, over an exchangeable path law in which cylinders over disjoint index blocks are independent.
• exchangeableSigma_trivial_of_infinitePi — the zero-one law for the i.i.d. product law P^{⊗ℕ} itself.

Everything else in this file is private proof infrastructure: the block permutation, the reindexed-cylinder change of variables, the cylinder approximation, and the disjoint-block product formula. The final approximation squeeze — arbitrarily close factoring approximants force measure 0 or 1 — is delegated to the shared zero-one criterion TauCeti.MeasureTheory.measure_eq_zero_or_one_of_forall_exists_symmDiff_lt_inter_eq_mul.

The argument

Approximate an exchangeable event by a cylinder over [0, N), then move that cylinder onto the disjoint block [N, 2N). The mover is Nat.blockSwap N, the half-swap of Fin (N + N) transported to ℕ: it is finitely supported, hence admissible for exchangeableSigma, so it fixes the event while preserving the law. Independence then factors the event against its own moved copy, and letting the approximation tighten gives q = q².

The independence step lives on the source space rather than on path space — iIndepFun.indepFun_finset applies to the coordinate tuples of X, and Measure.map_apply transfers the resulting identity to pathLaw μ X. Stating it directly for a path-space measure would first need a lemma transferring iIndepFun to the coordinate projections.

This discharges the Layer 2 target hewittSavage_trivial_of_iIndep of TauCetiRoadmap/Exchangeability/README.md, and supplies the Layer 2 input the roadmap records for the Layer 6 extreme-point corollary (the extreme exchangeable laws are exactly the i.i.d. laws).

References

• Edwin Hewitt and Leonard J. Savage, Symmetric measures on Cartesian products, Transactions of the American Mathematical Society 80 (1955), 470–501, https://doi.org/10.2307/1992999 — the original theorem, and the source the roadmap names for this target.
• Olav Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1.

No material is adapted from cameronfreer/exchangeability: that formalization does not carry this theorem, and the proof here is assembled from Mathlib's cylinder, approximation, and independence API.

theorem TauCeti.Probability.measure_eq_zero_or_one_of_exchangeableSigma {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hexch : ExchangeableLaw ρ) (hprod : ∀ {F G : Finset ℕ}, Disjoint F G → ∀ {S : Set (↥F → α)}, MeasurableSet S → ∀ {T : Set (↥G → α)}, MeasurableSet T → ρ (MeasureTheory.cylinder F S ∩ MeasureTheory.cylinder G T) = ρ (MeasureTheory.cylinder F S) * ρ (MeasureTheory.cylinder G T)) {s : Set (ℕ → α)} (hs : MeasurableSet s) : ρ s = 0 ∨ ρ s = 1

Zero-one law for exchangeable events, abstract form: an exchangeable path law in which cylinders over disjoint index blocks are independent gives every exchangeable event measure 0 or 1.

theorem TauCeti.Probability.hewittSavage_trivial_of_iIndep {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h_indep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) {s : Set (ℕ → α)} (hs : MeasurableSet s) : (pathLaw μ X) s = 0 ∨ (pathLaw μ X) s = 1

The Hewitt–Savage zero-one law. For an i.i.d. sequence, the exchangeable (symmetric) σ-algebra on path space is trivial: every exchangeable event has probability 0 or 1.

Kolmogorov's tail zero-one law does not subsume this: tail triviality needs only independence, whereas the symmetric σ-algebra can contain non-tail events — for measurable B with B ≠ ∅ and B ≠ Set.univ, the event {p | ∃ n, p n ∈ B} is permutation-invariant but not a tail event (see the module docstring). Identical distribution is used here to obtain exchangeability of the path law, which is what the argument consumes; it is not claimed to be necessary for the conclusion — measure_eq_zero_or_one_of_exchangeableSigma assumes exchangeability directly.

theorem TauCeti.Probability.exchangeableSigma_trivial_of_infinitePi {α : Type u_2} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) {s : Set (ℕ → α)} (hs : MeasurableSet s) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) s = 0 ∨ (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) s = 1

The zero-one law for an i.i.d. product law. Every exchangeable event has probability 0 or 1 under P^{⊗ℕ}.

This is hewittSavage_trivial_of_iIndep read for the product law itself rather than for a process carried by some other measure: under P^{⊗ℕ} the coordinates are independent and identically distributed, and the path law of the coordinate process is the product law back again.