Finite measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the type of finite measures on a given measurable space. When the underlying space has a topology and the measurable space structure (sigma algebra) is finer than the Borel sigma algebra, then the type of finite measures is equipped with the topology of weak convergence of measures. 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.

Main definitions #

The main definitions are

• the type measure_theory.finite_measure Ω with the topology of weak convergence;
• measure_theory.finite_measure.to_weak_dual_bcnn : 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 is used for the definition of the topology of weak convergence.

Main results #

• Finite measures μ on Ω give rise to continuous linear functionals on the space of bounded continuous nonnegative functions on Ω via integration: measure_theory.finite_measure.to_weak_dual_bcnn : finite_measure Ω → (weak_dual ℝ≥0 (Ω →ᵇ ℝ≥0))
• measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto: Convergence of finite measures is characterized by the convergence of integrals of all bounded continuous functions. This shows that the chosen definition of topology coincides with the common textbook definition of weak convergence of measures. A similar characterization by the convergence of integrals (in the measure_theory.lintegral sense) of all bounded continuous nonnegative functions is measure_theory.finite_measure.tendsto_iff_forall_lintegral_tendsto.

Implementation notes #

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

The implementation of measure_theory.finite_measure Ω and is directly as a subtype of measure_theory.measure Ω, and the coercion to a function is the composition ennreal.to_nnreal and the coercion to function of measure_theory.measure Ω. Another alternative would have been to use a bijection with measure_theory.vector_measure Ω ℝ≥0 as an intermediate step. Some considerations:

• 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 measure_theory.lintegral w.r.t. a coercion to measure_theory.measure Ω in any case.

References #

• Billingsley, Convergence of probability measures

Tags #

weak convergence of measures, finite measure

Finite measures #

In this section we define the Type of finite_measure Ω, when Ω is a measurable space. Finite measures on Ω are a module over ℝ≥0.

If Ω is moreover a topological space and the sigma algebra on Ω is finer than the Borel sigma algebra (i.e. [opens_measurable_space Ω]), then finite_measure Ω is equipped with the topology of weak convergence of measures. This is implemented by defining a pairing of finite measures μ on Ω with continuous bounded nonnegative functions f : Ω →ᵇ ℝ≥0 via integration, and using the associated weak topology (essentially the weak-star topology on the dual of Ω →ᵇ ℝ≥0).

Bounded convergence results for finite measures #

This section is about bounded convergence theorems for finite measures.

Weak convergence of finite measures with bounded continuous real-valued functions #

In this section we characterize the weak convergence of finite measures by the usual (defining) condition that the integrals of all bounded continuous real-valued functions converge.