# Documentation

Mathlib.MeasureTheory.Measure.Portmanteau

# Characterizations of weak convergence of finite measures and probability measures #

This file will provide portmanteau characterizations of the weak convergence of finite measures and of probability measures, i.e., the standard characterizations of convergence in distribution.

## Main definitions #

The topologies of weak convergence on the types of finite measures and probability measures are already defined in their corresponding files; no substantial new definitions are introduced here.

## Main results #

The main result will be the portmanteau theorem providing various characterizations of the weak convergence of measures (probability measures or finite measures). Given measures μs and μ on a topological space Ω, the conditions that will be proven equivalent (under quite general hypotheses) are:

(T) The measures μs tend to the measure μ weakly. (C) For any closed set F, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F). (O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G). (B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B).

The separate implications are:

• MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto is the implication (T) → (C).
• MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge is the equivalence (C) ↔ (O).
• MeasureTheory.tendsto_measure_of_null_frontier is the implication (O) → (B).
• MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure is the implication (B) → (C).

TODO:

• Prove the remaining implication (O) → (T) to complete the proof of equivalence of the conditions.

## Implementation notes #

Many of the characterizations of weak convergence hold for finite measures and are proven in that generality and then specialized to probability measures. Some implications hold with slightly more general assumptions than in the usual statement of portmanteau theorem. The full portmanteau theorem, however, is most convenient for probability measures on pseudo-emetrizable spaces with their Borel sigma algebras.

Some specific considerations on the assumptions in the different implications:

• MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto assumes PseudoEMetricSpace. The only reason is to have bounded continuous pointwise approximations to the indicator function of a closed set. Clearly for example metrizability or pseudo-emetrizability would be sufficient assumptions. The typeclass assumptions should be later adjusted in a way that takes into account use cases, but the proof will presumably remain essentially the same.
• Where formulations are currently only provided for probability measures, one can obtain the finite measure formulations using the characterization of convergence of finite measures by their total masses and their probability-normalized versions, i.e., by MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto.
• [Billingsley, Convergence of probability measures][billingsley1999]

## Tags #

weak convergence of measures, convergence in distribution, convergence in law, finite measure, probability measure