De Finetti's theorem in empirical form

The de Finetti endpoints of the conditional strong law: for an exchangeable process on a nonempty standard Borel space, the directing measure's mass on each fixed measurable set is the almost-sure limit of the process's empirical frequencies, and — once a compatible Polish topology on the state space is fixed — the directing measure is itself the almost-sure weak limit of the empirical measures.

These are the meeting point of two independent inputs, and it is why they live in their own module. The analytic content is ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae and ConditionallyIIDWith.tendsto_empiricalMeasure_ae, stated for a conditionally i.i.d. process and needing no standard-Borel structure; the existence of the directing measure for an exchangeable process is conditionallyIID_of_exchangeable, the de Finetti summit. Keeping the two apart lets a caller import the conditional strong law without also importing the summit, which is a substantially larger closure.

The two endpoints differ in what they assume of the state space, not merely in strength. [StandardBorelSpace α] selects no topology, so it supports the fixed-set statement but cannot even express weak convergence; the weak form therefore asks for a Polish topology and the Borel σ-algebra it generates, which in particular makes α standard Borel.

Main results

• deFinetti_tendsto_empiricalMeasure_apply — for an exchangeable process on a standard Borel state space, a directing measure whose mass on each fixed measurable set is recovered as the almost-sure limit of the empirical frequencies;
• deFinetti_empiricalMeasure — for an exchangeable process on a Polish state space, a directing measure that is the almost-sure weak limit of the empirical measures.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6's empirical form of the directing-measure theorem, in both its topology-free fixed-set version and its weak-convergence version.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005), §1.1.

No material is adapted from cameronfreer/exchangeability, which does not treat empirical measures.

theorem TauCeti.Probability.deFinetti_tendsto_empiricalMeasure_apply {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [StandardBorelSpace α] [Nonempty α] [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) : ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), ConditionallyIIDWith μ X ν ∧ ∀ (B : Set α), MeasurableSet B → ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => (↑(empiricalMeasure (fun (i : ℕ) => X i ω) n) B).toReal) Filter.atTop (nhds (↑(ν ω) B).toReal)

De Finetti's theorem in empirical-frequency form. An exchangeable process valued in a nonempty standard Borel space has a directing measure whose mass on each fixed measurable set is recovered, almost surely, as the limit of the empirical frequencies of the process.

The directing measure is thus not merely asserted to exist: each of its values is the pathwise limit of an explicit statistic of the process. The null set depends on the set tested, as it must. The weak-topology form of the same statement, testing against bounded continuous functions simultaneously, is deFinetti_empiricalMeasure below, which additionally assumes a compatible Polish topology on α and its Borel σ-algebra.

theorem TauCeti.Probability.deFinetti_empiricalMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [TopologicalSpace α] [PolishSpace α] [BorelSpace α] [Nonempty α] [MeasureTheory.IsFiniteMeasure μ] (hX : Exchangeable μ X) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) : ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), ConditionallyIIDWith μ X ν ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => empiricalMeasure (fun (i : ℕ) => X i ω) n) Filter.atTop (nhds (ν ω))

De Finetti's theorem in empirical-measure form. An exchangeable process valued in a nonempty Polish space, with its Borel σ-algebra, has a directing measure that is almost surely the weak limit of the empirical measures of the process — the limit is in the topology of convergence in distribution on ProbabilityMeasure α, so it tests against all bounded continuous functions simultaneously.

The directing measure is thus recovered from the process by an explicit pathwise limit, and not merely one measurable set at a time as in deFinetti_tendsto_empiricalMeasure_apply. A Polish topology is assumed rather than produced: [StandardBorelSpace α] alone fixes no topology on α, and different compatible topologies give different weak topologies on ProbabilityMeasure α.