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
f, the integration of
f against the
measure is continuous.
- 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
- Define the topologies on the above types.
Main results #
- Portmanteau theorem.
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
measure α, and the coercion to a function is the composition
and the coercion to function of
measure α. Another alternative would be to use a bijection
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
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
lintegralw.r.t. a coercion to
measure αin any case.
weak convergence of measures, finite measure, probability measure
Finite measures are defined as the subtype of measures that have the property of being finite measures (i.e., their total mass is finite).
A finite measure can be interpreted as a measure.
Coercion is an
Probability measures are defined as the subtype of measures that have the property of being probability measures (i.e., their total mass is one).
A probability measure can be interpreted as a measure.