De Finetti's theorem via L² averaging

This file is the endpoint of the martingale-free L² route to de Finetti's theorem. The route's substantive conclusion, Contractable.conditionallyIIDWith_directingProbabilityMeasure, names the tail-conditional directing measure and proves the joint-law disintegration of every finite block. Here that named witness is packaged into ConditionallyIID, and the standard exchangeable and equivalence forms are derived from the elementary implication lattice.

The suffix _viaL2 records the proof route. The corresponding unsuffixed public theorems in TauCeti.Probability.DeFinetti.Theorem use the reverse-martingale route and are deliberately not imported here. Thus importing this module gives a complete de Finetti theorem without importing reverse-martingale convergence or the unsuffixed summit.

Main results

• conditionallyIID_of_contractable_viaL2 — a contractable process is conditionally i.i.d.;
• deFinetti_viaL2 — an exchangeable process is conditionally i.i.d.;
• deFinetti_RyllNardzewski_equivalence_viaL2 — contractability is equivalent to the conjunction of exchangeability and conditional i.i.d.-ness.

These route wrappers are the final target of Layer 3 of TauCetiRoadmap/Exchangeability/README.md. They are not adapted from the legacy theorem wrappers in cameronfreer/exchangeability: those wrappers conclude only the mixture identity, whereas the results here package Tau Ceti's stronger joint-law disintegration.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1, Theorem 1.1.
• C. Ryll-Nardzewski, "On stationary sequences of random variables and the de Finetti equivalence", 1957.

theorem TauCeti.Probability.conditionallyIID_of_contractable_viaL2 {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : ConditionallyIID μ X

The contractable form of de Finetti's theorem via L² averaging. A contractable process valued in a nonempty standard Borel space is conditionally i.i.d.

The directing measure witnessing the conclusion is directingProbabilityMeasure μ X; its stronger witness-level statement is Contractable.conditionallyIIDWith_directingProbabilityMeasure.

theorem TauCeti.Probability.deFinetti_viaL2 {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX : Exchangeable μ X) : ConditionallyIID μ X

De Finetti's theorem via L² averaging. An exchangeable process valued in a nonempty standard Borel space is conditionally i.i.d.

theorem TauCeti.Probability.deFinetti_RyllNardzewski_equivalence_viaL2 {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) : Contractable μ X ↔ Exchangeable μ X ∧ ConditionallyIID μ X

The de Finetti--Ryll-Nardzewski equivalence via L² averaging. For a measurable process on a nonempty standard Borel state space, contractability is equivalent to being both exchangeable and conditionally i.i.d.