mathlib documentation

measure_theory.measure.finite_measure_weak_convergence

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:

Main definitions #

The main definitions are the

TODO:

Main results #

TODO:

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:

References #

Tags #

weak convergence of measures, finite measure, probability measure

def measure_theory.finite_measure (α : Type u_1) [measurable_space α] :
Type u_1

Finite measures are defined as the subtype of measures that have the property of being finite measures (i.e., their total mass is finite).

Equations

The (total) mass of a finite measure μ is μ univ, i.e., the cast to nnreal of (μ : measure α) univ.

Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem measure_theory.finite_measure.coe_zero {α : Type u_1} [measurable_space α] :
0 = 0
@[simp, norm_cast]
theorem measure_theory.finite_measure.coe_add {α : Type u_1} [measurable_space α] (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem measure_theory.finite_measure.coe_fn_add {α : Type u_1} [measurable_space α] (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp, norm_cast]

The pairing of a finite (Borel) measure μ with a nonnegative bounded continuous function is obtained by (Lebesgue) integrating the (test) function against the measure. This is finite_measure.test_against_nn.

Equations

Finite measures yield elements of the weak_dual of bounded continuous nonnegative functions via finite_measure.test_against_nn, i.e., integration.

Equations
def measure_theory.probability_measure (α : Type u_1) [measurable_space α] :
Type u_1

Probability measures are defined as the subtype of measures that have the property of being probability measures (i.e., their total mass is one).

Equations

A probability measure can be interpreted as a finite measure.

Equations

The pairing of a (Borel) probability measure μ with a nonnegative bounded continuous function is obtained by (Lebesgue) integrating the (test) function against the measure. This is probability_measure.test_against_nn.

Equations

Probability measures yield elements of the weak_dual of bounded continuous nonnegative functions via probability_measure.test_against_nn, i.e., integration.

Equations