The de Finetti measure is the mixing law

The development names the mixing law of an exchangeable process three times:

• deFinettiMeasure μ X, the law of the canonical tail directing measure (DeFinetti/Mixture.lean);
• the unique witness π produced by deFinetti_mixture (DeFinetti/Representation.lean);
• deFinettiEquiv.symm ρ, the mixing law read off an exchangeable path law (DeFinetti/Correspondence.lean).

This file proves they agree. The first is a construction on the sample space, the second an existential characterization of the path law, and the third the inverse of a bijection; without these identifications a caller holding one of them cannot use the theorems stated about the others.

Main results

• pathLaw_eq_bind_infinitePi_deFinettiMeasure_of_contractable and ..._of_exchangeable — the mixture representation directly from contractability or exchangeability, with no witness supplied by the caller.
• eq_deFinettiMeasure_of_pathLaw_eq_bind_infinitePi — every mixing law representing the path law is deFinettiMeasure; this is what identifies the deFinetti_mixture witness.
• deFinettiEquiv_symm_eq_deFinettiMeasure — the correspondence reads deFinettiMeasure off the packaged path law.

Hypotheses

The witness that drives everything here is Contractable.conditionallyIIDWith_directingProbabilityMeasure: a contractable process with measurable coordinates, valued in a nonempty standard Borel state space, under a finite measure, has directingProbabilityMeasure μ X as a directing measure. No standard-Borel hypothesis is imposed on the sample space Ω, so neither is one imposed below; a probability base measure is needed only because deFinettiMeasure is bundled as a ProbabilityMeasure.

[Nonempty α] cannot be dropped here even though a probability measure on Ω together with X 0 exhibits a point of α: it is not only a hypothesis. deFinettiMeasure is built from condDistrib, so the instance is needed to elaborate the statements themselves, not just to prove them.

The coordinates must be exactly measurable for a concrete reason that is not about deFinettiMeasure itself — that elaborates for an arbitrary X: Contractable.conditionallyIIDWith_directingProbabilityMeasure, which supplies the witness, asks for ∀ n, Measurable (X n).

Why the L² route supplies the witness

The theorems below carry no route suffix, yet the witness comes from the L² route. That is not a route claim: deFinettiMeasure is the law of directingProbabilityMeasure μ X, and the L² route's conditional summit is the one that names that object. The martingale route reaches the conditional summit through conditionallyIIDWith_of_contractable_pathSpace, whose witness lives on path space, and its mixture-side mixedIIDWith_of_contractable names the canonical directing measure only under [StandardBorelSpace Ω]. Taking the witness from the L² route is therefore what keeps that hypothesis out of these statements; a martingale-route proof would give a strictly weaker theorem, not a differently-named one.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6 (the mixture-of-product-measures form with π the unique law of ν) and Layer 8 (the affine correspondence). This file adds no new mathematics to either; it connects the objects those bullets produce.
• Olav Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1, Theorem 1.1.

theorem TauCeti.Probability.pathLaw_eq_bind_infinitePi_deFinettiMeasure_of_contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : pathLaw μ X = (↑(deFinettiMeasure μ X)).bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

The mixture representation of a contractable process, against its own de Finetti measure. Unlike pathLaw_eq_bind_infinitePi_deFinettiMeasure_of_mixedIIDWith, no witness is asked of the caller: the canonical directing measure is one, by Contractable.conditionallyIIDWith_directingProbabilityMeasure.

theorem TauCeti.Probability.pathLaw_eq_bind_infinitePi_deFinettiMeasure_of_exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : Exchangeable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : pathLaw μ X = (↑(deFinettiMeasure μ X)).bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P

The de Finetti representation of an exchangeable process, against its own de Finetti measure. This is deFinetti_mixture with the existential witness replaced by the canonical construction.

theorem TauCeti.Probability.eq_deFinettiMeasure_of_pathLaw_eq_bind_infinitePi {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) {π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α)} (hπ : pathLaw μ X = (↑π).bind fun (P : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑P) : π = deFinettiMeasure μ X

The de Finetti measure is the unique mixing law. Any probability measure on ProbabilityMeasure α representing the path law of an exchangeable process as an infinite-product mixture is deFinettiMeasure.

In particular the witness returned by deFinetti_mixture is this one, so a concrete mixing law established by any other route can be compared with the canonical construction.

Exchangeability is not assumed: hπ already exhibits the path law as a de Finetti barycenter, and every barycenter of a mixing probability law is an exchangeable path law.

theorem TauCeti.Probability.deFinettiEquiv_symm_eq_deFinettiMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) {ρ : { ρ : MeasureTheory.ProbabilityMeasure (ℕ → α) // ExchangeableLaw ↑ρ }} (hρ : ↑↑ρ = pathLaw μ X) : deFinettiEquiv.symm ρ = deFinettiMeasure μ X

The correspondence recovers the de Finetti measure. Reading the mixing law off the path law of an exchangeable process, through the inverse of deFinettiEquiv, gives the canonical deFinettiMeasure.

The packaged exchangeable law is taken as a hypothesis rather than constructed, so the caller may supply whichever bundling of pathLaw μ X is at hand. Exchangeability of the process is not assumed separately: ρ.2 and hρ already say the path law is exchangeable.