The de Finetti barycenter of a mixing law

De Finetti's representation is a map in one direction and a theorem in the other. This file builds the map. For a measure π on ProbabilityMeasure α — a mixing law — the de Finetti barycenter

deFinettiBarycenter π = ∫ P^{⊗ℕ} dπ(P)

is the Measure.bind of π against the countable-power kernel P ↦ P^{⊗ℕ}, equivalently the barycenter (Measure.join) of the pushforward of π along P ↦ P^{⊗ℕ}; that second reading is the one that makes the representation an ergodic decomposition, since every P^{⊗ℕ} is an extreme exchangeable law (infinitePi_mem_extremePoints_exchangeable). The definition accepts an arbitrary measure π; when π is a probability measure the barycenter is the law on ℕ → α of a sequence drawn i.i.d. from a π-random probability measure.

The map is affine in the mixing law — deFinettiBarycenter_add and Mathlib's Measure.bind_smul — sends probability measures to exchangeable probability measures, and, by de Finetti's theorem, hits every exchangeable probability law exactly once (ExchangeableLaw.existsUnique_mixingLaw). The packaging of that bijection as an equivalence, and its restriction to point masses, is in TauCeti.Probability.DeFinetti.Correspondence.

This is the object the Layer 8 bullet of TauCetiRoadmap/Exchangeability/README.md — "package p ↦ p^{⊗ℕ} and the de Finetti barycenter as an affine correspondence between mixing laws and exchangeable path laws" — asks for. The expression π.bind (P ↦ P^{⊗ℕ}) already occurs unnamed throughout the de Finetti development (deFinetti_mixture, mixedIID_mixingLaw_unique, Measure.ext_of_bind_infinitePi_eq); naming it is what lets the correspondence be stated.

Main results

• deFinettiBarycenter — the mixture of countable powers along a mixing law.
• deFinettiBarycenter_dirac — a point mass mixes to a single i.i.d. law.
• deFinettiBarycenter_zero, deFinettiBarycenter_add, deFinettiBarycenter_smul — affinity in the mixing law.
• map_pi_deFinettiBarycenter — naturality in the state space: a coordinatewise pushforward of a barycenter is the barycenter of the pushed-forward mixing law.
• exchangeableLaw_deFinettiBarycenter — every barycenter of a mixing probability law is an exchangeable path law.
• ExchangeableLaw.existsUnique_mixingLaw — conversely, an exchangeable probability law on ℕ → α is the barycenter of exactly one mixing law, for α standard Borel.

References

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

No material is adapted from cameronfreer/exchangeability, which carries the mixture representation only as an unnamed bind expression and does not package the correspondence.

noncomputable def TauCeti.Probability.deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) : MeasureTheory.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.

Equations

• TauCeti.Probability.deFinettiBarycenter π = π.bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

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

The barycenter unfolded as a Measure.bind against the countable-power kernel. This is the form in which the surrounding development states the mixture representation, so it is the bridge to deFinetti_mixture, mixedIID_mixingLaw_unique and Measure.ext_of_bind_infinitePi_eq.

theorem TauCeti.Probability.deFinettiBarycenter_eq_join_map {α : Type u_1} [MeasurableSpace α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) : deFinettiBarycenter π = (MeasureTheory.Measure.map (fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.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 TauCeti.Probability.deFinettiBarycenter_apply {α : Type u_1} [MeasurableSpace α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) {s : Set (ℕ → α)} (hs : MeasurableSet s) : (deFinettiBarycenter π) s = ∫⁻ (P : MeasureTheory.ProbabilityMeasure α), (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) s ∂π

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

@[simp]

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

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

instance TauCeti.Probability.isProbabilityMeasure_deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) [MeasureTheory.IsProbabilityMeasure π] : MeasureTheory.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 TauCeti.Probability.deFinettiBarycenter_zero {α : Type u_1} [MeasurableSpace α] : deFinettiBarycenter 0 = 0

The zero mixing law has the zero barycenter.

@[simp]

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

The barycenter is additive in the mixing law.

@[simp]

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

The barycenter is homogeneous in the mixing law.

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

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.

theorem TauCeti.Probability.exchangeableLaw_deFinettiBarycenter {α : Type u_1} [MeasurableSpace α] {π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)} [MeasureTheory.IsProbabilityMeasure π] : ExchangeableLaw (deFinettiBarycenter π)

A barycenter is an exchangeable path law. Drawing P from π and then an i.i.d. P-sequence produces a law invariant under every permutation of the time coordinate.

The witness is the canonical conditionally i.i.d. construction iidMixtureLaw π id, whose coordinate process is exchangeable and whose path law is this barycenter.

theorem TauCeti.Probability.ExchangeableLaw.existsUnique_mixingLaw {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) : ∃! π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α), ρ = deFinettiBarycenter ↑π

The mixing law of an exchangeable path law. Over a standard Borel state space, an exchangeable probability measure on ℕ → α is the de Finetti barycenter of exactly one mixing law.

This is the path-law form of deFinetti_mixture, obtained by taking the coordinate process of ρ itself: existence is de Finetti's theorem and uniqueness is injectivity of the mixture. Like deFinetti_mixture, it needs no nonemptiness hypothesis on the state space.