Weak convergence of (finite) measures #

This file will define the topology of weak convergence of finite measures and probability measures on topological spaces. The topology of weak convergence is the coarsest topology w.r.t. which for every bounded continuous ℝ≥0-valued function f, the integration of f against the measure is continuous.

TODOs:

• Define the topologies (the current version only defines the types) via weak_dual ℝ≥0 (α →ᵇ ℝ≥0).
• Prove that an equivalent definition of the topologies is obtained requiring continuity of integration of bounded continuous ℝ-valued functions instead.
• Include the portmanteau theorem on characterizations of weak convergence of (Borel) probability measures.

Main definitions #

The main definitions are the

• types finite_measure α and probability_measure α;
• to_weak_dual_bounded_continuous_nnreal : finite_measure α → (weak_dual ℝ≥0 (α →ᵇ ℝ≥0)) allowing to interpret a finite measure as a continuous linear functional on the space of bounded continuous nonnegative functions on α. This will be used for the definition of the topology of weak convergence.

TODO:

• Define the topologies on the above types.

Main results #

• Finite measures μ on α give rise to continuous linear functionals on the space of bounded continuous nonnegative functions on α via integration: to_weak_dual_of_bounded_continuous_nnreal : finite_measure α → (weak_dual ℝ≥0 (α →ᵇ ℝ≥0)).

TODO:

• Portmanteau theorem.

Notations #

No new notation is introduced.

Implementation notes #

The topology of weak convergence of finite Borel measures will be defined using a mapping from finite_measure α to weak_dual ℝ≥0 (α →ᵇ ℝ≥0), inheriting the topology from the latter.

The current implementation of finite_measure α and probability_measure α is directly as subtypes of measure α, and the coercion to a function is the composition ennreal.to_nnreal and the coercion to function of measure α. Another alternative would be to use a bijection with vector_measure α ℝ≥0 as an intermediate step. The choice of implementation should not have drastic downstream effects, so it can be changed later if appropriate.

Potential advantages of using the nnreal-valued vector measure alternative:

• The coercion to function would avoid need to compose with ennreal.to_nnreal, the nnreal-valued API could be more directly available. Potential drawbacks of the vector measure alternative:
• The coercion to function would lose monotonicity, as non-measurable sets would be defined to have measure 0.
• No integration theory directly. E.g., the topology definition requires lintegral w.r.t. a coercion to measure α in any case.

References #

• Billingsley, Convergence of probability measures

Tags #

weak convergence of measures, finite measure, probability measure