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 types finite_measure α and probability_measure α.

TODO:

Main results #

None yet.

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
@[simp]
theorem measure_theory.finite_measure.coe_zero {α : Type u_1} [measurable_space α] :
0 = 0
@[simp]
theorem measure_theory.finite_measure.coe_add {α : Type u_1} [measurable_space α] (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp]
@[simp]
@[simp]
theorem measure_theory.finite_measure.coe_fn_add {α : Type u_1} [measurable_space α] (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp]
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