Extreme exchangeable laws

The extreme points of the convex set of exchangeable probability measures on ℕ → α are exactly the i.i.d. product laws. The main theorem exchangeable_extreme_iff_iid states this using Mathlib's Set.extremePoints for the natural ℝ≥0∞-module structure on measures.

The exchangeable probability laws are the probability laws invariant under the action of the finitely supported permutations of ℕ (exchangeableLaw_iff_smulInvariantMeasure). Extremality among them is therefore ergodicity of that action, by the general characterisation ErgodicSMul.iff_mem_extremePoints for a countable group; ergodicity is triviality of the exchangeable σ-algebra (exchangeableSigma_trivial_iff_ergodicSMul); and, for a standard Borel state space, triviality is the i.i.d. property (exchangeableSigma_trivial_iff_iid). The implication from i.i.d. to extreme needs no standard Borel hypothesis.

The one-sided shift ergodicity of an i.i.d. law, ergodic_shift_infinitePi_const, is recorded here as well: shift-invariant events are exchangeable events, so the Hewitt–Savage zero-one law applies.

Main results

• exchangeableProbabilityMeasures, with its membership and convexity lemmas, and exchangeableProbabilityMeasures_eq — the exchangeable probability laws are the invariant probability laws of the finitary action.
• ergodic_shift_infinitePi_const — an i.i.d. product law is ergodic for the one-sided shift.
• infinitePi_mem_extremePoints_exchangeable — an i.i.d. product law is an extreme exchangeable law, over an arbitrary measurable space.
• exchangeable_extreme_iff_iid — the extreme exchangeable probability laws are exactly the i.i.d. product laws.

References

• Olav Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1.
• Edwin Hewitt and Leonard J. Savage, Symmetric measures on Cartesian products, Transactions of the American Mathematical Society 80 (1955), 470–501.

def TauCeti.Probability.exchangeableProbabilityMeasures (α : Type u_2) [MeasurableSpace α] : Set (MeasureTheory.Measure (ℕ → α))

The convex set of exchangeable probability laws on path space.

Equations

• TauCeti.Probability.exchangeableProbabilityMeasures α = {ν : MeasureTheory.Measure (ℕ → α) | TauCeti.Probability.ExchangeableLaw ν ∧ MeasureTheory.IsProbabilityMeasure ν}

@[simp]

theorem TauCeti.Probability.mem_exchangeableProbabilityMeasures_iff {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure (ℕ → α)} : ν ∈ exchangeableProbabilityMeasures α ↔ ExchangeableLaw ν ∧ MeasureTheory.IsProbabilityMeasure ν

Membership in the exchangeable probability laws.

theorem TauCeti.Probability.exchangeableProbabilityMeasures_eq {α : Type u_1} [MeasurableSpace α] : exchangeableProbabilityMeasures α = MeasureTheory.invariantMeasuresOfMeasureUnivEq FinitaryPerm (ℕ → α) 1

The exchangeable probability laws are the invariant measures of total mass one of the finitary permutation action.

theorem TauCeti.Probability.convex_exchangeableProbabilityMeasures {α : Type u_1} [MeasurableSpace α] : Convex ENNReal (exchangeableProbabilityMeasures α)

The exchangeable probability laws form a convex set.

theorem TauCeti.Probability.ergodic_shift_infinitePi_const {α : Type u_1} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) : Ergodic (shift α) (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P)

An i.i.d. infinite product law is ergodic for the one-sided shift.

The shift-invariant σ-algebra is contained in the exchangeable σ-algebra, and the coordinate process is independent and identically distributed under the product law, so Hewitt–Savage makes every shift-invariant event null or conull.

theorem TauCeti.Probability.infinitePi_mem_extremePoints_exchangeable {α : Type u_1} [MeasurableSpace α] (P : MeasureTheory.ProbabilityMeasure α) : (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) ∈ Set.extremePoints ENNReal (exchangeableProbabilityMeasures α)

An i.i.d. law is an extreme exchangeable law. The infinite product is ergodic for the finitary permutation action, hence extreme among its invariant probability laws, which are the exchangeable ones.

theorem TauCeti.Probability.exchangeable_extreme_iff_iid {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] : ρ ∈ Set.extremePoints ENNReal (exchangeableProbabilityMeasures α) ↔ ∃ (P : MeasureTheory.ProbabilityMeasure α), ρ = MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

The extreme exchangeable laws are exactly the i.i.d. laws. For a standard Borel state space, a probability measure on ℕ → α is an extreme point of the set of exchangeable probability measures if and only if it is an infinite product P^{⊗ℕ} for some probability measure P on α: extremality is ergodicity of the finitary permutation action, which is triviality of the exchangeable σ-algebra, which is the i.i.d. property.