Zero-one criteria and almost surely constant maps

A set under a finite measure has mass 0 or 1 if it admits arbitrarily close pairs of approximants whose intersection mass factors. No measurability of these sets is required. This is the approximation step of the Hewitt–Savage zero-one law and of dissociated-array ergodicity.

A zero-one measure gives every measurable set mass 0 or 1. Mathlib's MeasureTheory.IsZeroOneMeasure.exists_eq_dirac identifies such a measure with a Dirac mass, but only when the carrier is standard Borel. This file records the form that survives on an arbitrary carrier: a measurable map into a standard Borel space is almost surely constant, because its pushforward is again a zero-one probability measure and is therefore Dirac.

The carrier itself needs no Borel structure, so this applies to a space that carries a measurable map into a standard Borel space without being one — for instance ProbabilityMeasure α for a countably generated α, which TauCeti.MeasureTheory.IsZeroOneMeasure.exists_eq_dirac_probabilityMeasure evaluates into a countable power of ℝ≥0∞.

Main results

• TauCeti.MeasureTheory.measure_eq_zero_or_one_of_forall_exists_symmDiff_lt_inter_eq_mul: arbitrarily close factoring approximants force a zero-one set.

• TauCeti.MeasureTheory.IsZeroOneMeasure.exists_ae_eq_const: under a zero-one measure, an almost-everywhere measurable map into a standard Borel space agrees almost everywhere with a single value.

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.

• Olav Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1.

theorem TauCeti.MeasureTheory.measure_eq_zero_or_one_of_forall_exists_symmDiff_lt_inter_eq_mul {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {s : Set Ω} (happrox : ∀ (ε : ℝ), 0 < ε → ∃ (t : Set Ω) (t' : Set Ω), μ.real (symmDiff t s) < ε ∧ μ.real (symmDiff t' s) < ε ∧ μ.real (t ∩ t') = μ.real t * μ.real t') : μ s = 0 ∨ μ s = 1

Arbitrarily close factoring approximants force a zero-one set. Suppose that for every ε > 0, the set s is within ε in symmetric-difference measure of two sets t and t' whose intersection mass factors. Then s has measure 0 or 1.

The sets need not be measurable, and the approximants need not have the same measure; only the displayed factorization of their intersection is used.

theorem TauCeti.MeasureTheory.IsZeroOneMeasure.exists_ae_eq_const {Ω : Type u_1} {β : Type u_2} [MeasurableSpace Ω] [MeasurableSpace β] [StandardBorelSpace β] {π : MeasureTheory.Measure Ω} [NeZero π] [MeasureTheory.IsZeroOneMeasure π] {f : Ω → β} (hf : AEMeasurable f π) : ∃ (q : β), ∀ᵐ (ω : Ω) ∂π, f ω = q

A zero-one law is almost surely constant along a measurable map. The pushforward of a nonzero zero-one measure along f is again a zero-one probability measure; on a standard Borel space it is therefore a Dirac mass at some q, and f equals q almost everywhere.

The carrier Ω needs no topological or Borel structure of its own, and f need only be almost-everywhere measurable.