The de Finetti correspondence #
De Finetti's theorem says that the barycenter map π ↦ ∫ P^{⊗ℕ} dπ(P) is a bijection from mixing
laws onto exchangeable path laws. This file packages that bijection as an equivalence
deFinettiEquiv :
ProbabilityMeasure (ProbabilityMeasure α) ≃ {ρ : ProbabilityMeasure (ℕ → α) // ExchangeableLaw ρ}
for a standard Borel state space α, and identifies its point masses.
Injectivity is Measure.ext_of_bind_infinitePi_eq, surjectivity is
ExchangeableLaw.existsUnique_mixingLaw — de Finetti's theorem in path-law form. The inverse
deFinettiEquiv.symm is therefore a genuine construction: it reads the mixing law off an
exchangeable law.
The correspondence is affine, deFinettiBarycenter_add and deFinettiBarycenter_smul giving
the mixture identity on the barycenter side and deFinettiEquiv_convexComb /
deFinettiEquiv_symm_convexComb stating it for the bundled objects on both sides of the
equivalence; and it takes the point masses of
ProbabilityMeasure α exactly to the extreme exchangeable laws
(deFinettiBarycenter_mem_extremePoints_iff, deFinettiEquiv_dirac). Reading
deFinettiBarycenter as deFinettiBarycenter_eq_join_map does, this is the canonical
decomposition of an exchangeable law over the extreme — equivalently the
i.i.d. — exchangeable laws: the mixing law is unique, and the path laws it averages are extreme.
This settles the Layer 8 bullet "the affine and ergodic decomposition of exchangeable laws" in
TauCetiRoadmap/Exchangeability/README.md. Together with exchangeableSigma_trivial_iff_iid,
exchangeableSigma_trivial_iff_ergodicSMul and exchangeable_extreme_iff_iid, this correspondence
identifies the product — equivalently extreme — components with the ergodic components for the
finitely supported permutation action, which that bullet sequences after the ErgodicSMul interface
of Layer 6. Those equivalences compose directly; no additional correspondence declaration is
required.
⚠ The action is the finitely supported permutations of the time index. Ergodicity for it is a
different statement from ergodicity of the one-sided shift, which concerns the smaller σ-algebra of
shift-invariant events; see PathSpace/Exchangeable/Ergodic.lean.
Main results #
deFinettiEquiv— mixing laws correspond bijectively to exchangeable path laws.deFinettiEquiv_dirac,deFinettiEquiv_symm_eq_dirac— a point mass corresponds to an i.i.d. law, in both directions.deFinettiEquiv_convexComb,deFinettiEquiv_symm_convexComb— the correspondence and its inverse are affine, stated at the bundled level withProbabilityMeasure.convexCombandexchangeableLawConvexComb.deFinettiBarycenter_mem_extremePoints_iff— a barycenter is an extreme exchangeable law exactly when its mixing law is a point mass.
References #
- Olav Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1, Theorem 1.1.
- David Aldous, Exchangeability and related topics, École d'Été de Probabilités de Saint-Flour XIII, 1983, §3, for the affine and extreme-point reading of the representation.
No material is adapted from cameronfreer/exchangeability, which does not package the
representation as a correspondence.
The de Finetti correspondence. Over a standard Borel state space, the de Finetti
barycenter is a bijection from mixing laws — probability measures on ProbabilityMeasure α — onto
exchangeable probability measures on ℕ → α.
The forward map is deFinettiBarycenter; the inverse sends an exchangeable law to its mixing law.
Injectivity is uniqueness of the mixing law and surjectivity is de Finetti's theorem, so the
equivalence is exactly the content of ExchangeableLaw.existsUnique_mixingLaw in bijective
form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of the correspondence really is the mixing law: the barycenter of the mixing law of an exchangeable law recovers that law.
The mixing law is characterized by its barycenter: a mixing law whose barycenter is ρ is
the mixing law of ρ.
Point masses correspond to i.i.d. laws. A mixing law concentrated at P corresponds to
the i.i.d. law P^{⊗ℕ}.
The mixing law of an i.i.d. law is a point mass, the inverse reading of
deFinettiEquiv_dirac: an exchangeable law that happens to be P^{⊗ℕ} has δ_P as its mixing
law.
Affinity #
The correspondence is affine, and this section says so at the bundled level, with no coercion to
Measure on either side of the equations.
There is no AffineMap or AffineEquiv to be had: ProbabilityMeasure is not a module over
anything, carrying neither addition nor a scalar action, only the convex structure inherited from
the ambient Measure cone. ProbabilityMeasure.convexComb names that convex structure, and
exchangeableLawConvexComb carries it to the subtype of exchangeable laws; both are generic, so
they live outside this module. Affinity is then two equations between bundled objects.
Weights are arbitrary elements of ℝ≥0∞ summing to 1. Normalization is not decorative: without
it the combination is not a probability measure, so neither side of either equation would typecheck.
The unbundled statements without it are deFinettiBarycenter_add and deFinettiBarycenter_smul.
The correspondence is affine. It carries the convex combination of two mixing laws to the convex combination, with the same weights, of their exchangeable path laws.
The inverse correspondence is affine: decomposing an exchangeable law as a convex combination decomposes its mixing law the same way.
Formally this is the previous theorem read through the bijection, but the bijection is where
de Finetti's theorem sits: surjectivity of deFinettiEquiv is the representation theorem, and
injectivity is uniqueness of the mixing law.
The extreme fibres of the correspondence are exactly the point masses. The de Finetti barycenter of a mixing law is an extreme exchangeable probability law if and only if that mixing law is a Dirac mass.
Combined with deFinettiBarycenter_eq_join_map, this is the canonical decomposition an
exchangeable law admits: it is the barycenter of a unique law on path laws, and that law is
carried by the extreme — equivalently i.i.d. — exchangeable laws
(infinitePi_mem_extremePoints_exchangeable), degenerating exactly on the extreme points
themselves.