The empirical measures of a conditionally i.i.d. process converge weakly

The conditional strong law gives, for each fixed measurable set, almost-sure convergence of the empirical frequencies of a conditionally i.i.d. process to the mass the directing measure gives that set. This file makes the limit a statement about the empirical measures themselves: almost surely, empiricalMeasure (X · ω) n → ν ω in the topology of convergence in distribution on ProbabilityMeasure α.

Weak convergence tests against all bounded continuous functions at once, so the null set has to be chosen before the test function is seen, and the fixed-set statement cannot simply be quantified afterwards — outside a countable family of sets that interchange is false (see ConditionallyIID/StrongLaw.lean). What makes the upgrade go through is that a second-countable topology has a countable test class: the finite intersections of a countable basis, on which ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae_forall provides a single null set, and from which IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem recovers weak convergence — they form a π-system containing arbitrarily small neighbourhoods of every point.

The hypotheses on the state space are topological, not standard Borel: a second-countable topology whose open sets are measurable is all the argument uses. In particular a Polish space with its Borel σ-algebra qualifies, which is the form in which the roadmap states the result.

Main results

• ConditionallyIIDWith.tendsto_empiricalMeasure_ae — almost surely, the empirical measures converge weakly to the directing measure.

The de Finetti endpoint, where the directing measure of an exchangeable process has to be produced first, is deFinetti_empiricalMeasure in DeFinetti/EmpiricalMeasure.lean.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6, weak empirical-measure convergence.
• 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.ConditionallyIIDWith.tendsto_empiricalMeasure_ae {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => empiricalMeasure (fun (i : ℕ) => X i ω) n) Filter.atTop (nhds (ν ω))

The empirical measures of a conditionally i.i.d. process converge weakly to its directing measure, almost surely. The convergence is in the topology of convergence in distribution on ProbabilityMeasure α, and the null set is one and the same for every test function.

This is the measure-valued form of ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae, which gives the same limit one measurable set at a time. It does not follow by interchanging the quantifiers there, since no null set serves every measurable set at once; second countability is what makes countably many instances suffice, through ConditionallyIIDWith.tendsto_empiricalMeasure_apply_ae_forall.