The zero-one characterization of product laws

An exchangeable law on ℕ → α has trivial exchangeable σ-algebra exactly when it is an infinite product law:

exchangeableSigma_trivial_iff_iid.

The two directions

The product-to-zero-one direction is Hewitt–Savage, packaged for the product law itself as exchangeableSigma_trivial_of_infinitePi.

The converse is the substantive half, and it runs at the level of the mixing law rather than the directing map. The canonical witness directingProbabilityMeasure is tailProcess-measurable, and pathTail_le_exchangeableSigma puts the path tail inside exchangeableSigma, so every preimage ν ⁻¹' A is an exchangeable event. Triviality therefore makes ρ.map ν a zero-one measure on ProbabilityMeasure α, hence a Dirac measure by IsZeroOneMeasure.exists_eq_dirac_probabilityMeasure, and the de Finetti mixture representation pathLaw_eq_bind_infinitePi_of_mixedIIDWith collapses to a single product.

Working at the mixing-law level avoids needing a general "measurable into ProbabilityMeasure α implies almost everywhere constant" interface: the Giry-specific Dirac theorem is exactly the tool for this situation. Note that mixedIID_mixingLaw_unique alone does not give the converse — uniqueness of the mixing law is not the same as its being a point mass.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6, the exchangeableSigma_trivial_iff_iid interface among the equivalent characterizations of product laws.

theorem TauCeti.Probability.infinitePi_of_exchangeableSigma_trivial {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) (htriv : ∀ (s : Set (ℕ → α)), MeasurableSet s → ρ s = 0 ∨ ρ s = 1) : ∃ (P : MeasureTheory.ProbabilityMeasure α), ρ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

A trivial exchangeable σ-algebra forces an i.i.d. law. If every exchangeable event has probability 0 or 1 under an exchangeable law ρ, then ρ is an infinite product P^{⊗ℕ}.

theorem TauCeti.Probability.exchangeableSigma_trivial_iff_iid {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) : (∀ (s : Set (ℕ → α)), MeasurableSet s → ρ s = 0 ∨ ρ s = 1) ↔ ∃ (P : MeasureTheory.ProbabilityMeasure α), ρ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

The zero-one characterization of product laws. For a standard Borel state space, an exchangeable probability law on ℕ → α has trivial exchangeable σ-algebra exactly when it is an infinite product law.