Mixtures of i.i.d. path laws

The de Finetti barycenter of a measure π on ProbabilityMeasure α is the path-space measure ∫ P^{⊗ℕ} dπ(P). This construction needs only a measurable state space and an arbitrary mixing measure. It is useful independently of any representation theorem: draw a probability measure, then draw an i.i.d. path from it.

This file supplies evaluation on measurable events, the point-mass and zero cases, preservation of probability measures, additivity and homogeneity in the mixing measure, and compatibility with coordinatewise measurable pushforwards. The symmetry and uniqueness properties of the mixture belong in TauCeti.Probability.DeFinetti.Barycenter.

References

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

noncomputable def MeasureTheory.Measure.deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] (π : Measure (ProbabilityMeasure α)) : Measure (ℕ → α)

The de Finetti barycenter of a mixing law π on ProbabilityMeasure α: the measure ∫ P^{⊗ℕ} dπ(P) on ℕ → α mixing the countable powers against π. For π a probability measure this is the law of a sequence drawn i.i.d. from a π-random probability measure.

theorem MeasureTheory.Measure.deFinettiBarycenter_def {α : Type u_1} [MeasurableSpace α] (π : Measure (ProbabilityMeasure α)) : π.deFinettiBarycenter = π.bind fun (P : ProbabilityMeasure α) => infinitePi fun (x : ℕ) => ↑P

The barycenter unfolded as a Measure.bind against the countable-power kernel. This is the form used to evaluate mixtures and to compare their finite-dimensional marginals.

theorem MeasureTheory.Measure.deFinettiBarycenter_eq_join_map {α : Type u_1} [MeasurableSpace α] (π : Measure (ProbabilityMeasure α)) : π.deFinettiBarycenter = (map (fun (P : ProbabilityMeasure α) => infinitePi fun (x : ℕ) => ↑P) π).join

The barycenter as the Measure.join of the pushforward of the mixing measure along P ↦ P^{⊗ℕ}: the mixture representation read as a barycenter of measures on ℕ → α rather than of measures on α. For π a probability measure this pushforward is the law of P^{⊗ℕ} under a π-random P.

theorem MeasureTheory.Measure.deFinettiBarycenter_apply {α : Type u_1} [MeasurableSpace α] (π : Measure (ProbabilityMeasure α)) {s : Set (ℕ → α)} (hs : MeasurableSet s) : π.deFinettiBarycenter s = ∫⁻ (P : ProbabilityMeasure α), (infinitePi fun (x : ℕ) => ↑P) s ∂π

Evaluation of a barycenter on a measurable set: the π-average of the countable-power masses.

@[simp]

theorem MeasureTheory.Measure.deFinettiBarycenter_dirac {α : Type u_1} [MeasurableSpace α] (P : ProbabilityMeasure α) : (dirac P).deFinettiBarycenter = infinitePi fun (x : ℕ) => ↑P

A point mass mixing law has the corresponding i.i.d. law as its barycenter.

instance MeasureTheory.Measure.isProbabilityMeasure_deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] (π : Measure (ProbabilityMeasure α)) [IsProbabilityMeasure π] : IsProbabilityMeasure π.deFinettiBarycenter

The barycenter of a probability mixing law is a probability measure: every countable power of a probability measure is one, so the mixture keeps the total mass of π.

@[simp]

theorem MeasureTheory.Measure.deFinettiBarycenter_zero {α : Type u_1} [MeasurableSpace α] : deFinettiBarycenter 0 = 0

The zero mixing law has the zero barycenter.

@[simp]

theorem MeasureTheory.Measure.deFinettiBarycenter_add {α : Type u_1} [MeasurableSpace α] (π₁ π₂ : Measure (ProbabilityMeasure α)) : (π₁ + π₂).deFinettiBarycenter = π₁.deFinettiBarycenter + π₂.deFinettiBarycenter

The barycenter is additive in the mixing law.

@[simp]

theorem MeasureTheory.Measure.deFinettiBarycenter_smul {α : Type u_1} [MeasurableSpace α] (c : ENNReal) (π : Measure (ProbabilityMeasure α)) : (c • π).deFinettiBarycenter = c • π.deFinettiBarycenter

The barycenter is homogeneous in the mixing law.

theorem MeasureTheory.Measure.map_pi_deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] {β : Type u_2} [MeasurableSpace β] (π : Measure (ProbabilityMeasure α)) {f : α → β} (hf : Measurable f) : map (fun (x : ℕ → α) (i : ℕ) => f (x i)) π.deFinettiBarycenter = (map (fun (P : ProbabilityMeasure α) => P.map f) π).deFinettiBarycenter

The barycenter is natural in the state space. Pushing every coordinate of a barycenter forward by a measurable f : α → β gives the barycenter of the mixing law pushed forward by P ↦ P.map f: drawing P from π and then an i.i.d. P-sequence, and afterwards applying f to each term, is the same as drawing P.map f and then an i.i.d. sequence from it.