Exchangeable laws

A family of random variables indexed by ι with values in α is exchangeable when its law, a measure on ι → α, is unchanged by permuting the indices. The permutations act on ι → α by precomposition, as the domain action (Equiv.Perm ι)ᵈᵐᵃ ((DomMulAct.mk σ • x) i = x (σ i)), and Exchangeable μ is invariance under that action, SMulInvariantMeasure. Random partitions are exchangeable in the same sense, for the action of the permutations on partitions. On a countable space with measurable singletons, invariance is invariance of the point masses.

Main definitions

• ProbabilityTheory.Exchangeable μ: every permutation of the indices leaves μ unchanged.

Main results

• ProbabilityTheory.smulInvariantMeasure_of_measure_singleton: on a countable space with measurable singletons, a measure is invariant under a group action when moving a point never changes its mass.
• ProbabilityTheory.exchangeable_of_measure_singleton: the same for exchangeability.

Implementation notes

For infinite ι the usual definition asks for invariance only under the permutations that move finitely many indices; Exchangeable asks for all of them, which de Finetti's theorem shows equivalent on standard Borel spaces but which is not proved here. [UPSTREAM] candidate: mathlib has no notion of exchangeability.

References

• [Pit06]

theorem ProbabilityTheory.smulInvariantMeasure_of_measure_singleton {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MeasurableSpace X] [Countable X] [MeasurableSingletonClass X] {ν : MeasureTheory.Measure X} (h : ∀ (g : G) (x : X), ν {g • x} = ν {x}) : MeasureTheory.SMulInvariantMeasure G X ν

On a countable space with measurable singletons, a measure is invariant under a group action as soon as moving a point never changes its mass.

@[reducible, inline]

abbrev ProbabilityTheory.Exchangeable {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure (ι → α)) : Prop

The law μ of an ι-indexed family is exchangeable when every permutation of the indices, acting by precomposition, leaves it unchanged.

Equations

• ProbabilityTheory.Exchangeable μ = MeasureTheory.SMulInvariantMeasure (Equiv.Perm ι)ᵈᵐᵃ (ι → α) μ

theorem ProbabilityTheory.exchangeable_of_measure_singleton {ι : Type u_1} {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure (ι → α)} [Countable (ι → α)] [MeasurableSingletonClass (ι → α)] (h : ∀ (x : ι → α) (σ : Equiv.Perm ι), μ {x ∘ ⇑σ} = μ {x}) : Exchangeable μ

On a countable space with measurable singletons, a law is exchangeable as soon as permuting a point never changes its mass.