# mathlibdocumentation

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:

• 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 α.

TODO:

• Define the topologies on the above types.

## Main results #

None yet.

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.

## Tags #

weak convergence of measures, finite measure, probability measure

def measure_theory.finite_measure (α : Type u_1)  :
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
@[instance]

A finite measure can be interpreted as a measure.

Equations
@[instance]
@[instance]
def measure_theory.finite_measure.has_coe_to_fun {α : Type u_1}  :
(λ (_x : , set αℝ≥0)
Equations
@[simp]
@[simp]
theorem measure_theory.finite_measure.val_eq_to_measure {α : Type u_1}  :
ν.val = ν

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.ennreal_mass {α : Type u_1}  :
(μ.mass) =
@[instance]
def measure_theory.finite_measure.has_zero {α : Type u_1}  :
Equations
@[instance]
def measure_theory.finite_measure.inhabited {α : Type u_1}  :
Equations
@[instance]
def measure_theory.finite_measure.has_add {α : Type u_1}  :
Equations
@[instance]
Equations
@[simp]
theorem measure_theory.finite_measure.coe_zero {α : Type u_1}  :
0 = 0
@[simp]
theorem measure_theory.finite_measure.coe_add {α : Type u_1} (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp]
theorem measure_theory.finite_measure.coe_smul {α : Type u_1} (c : ℝ≥0)  :
(c μ) = c μ
@[simp]
theorem measure_theory.finite_measure.coe_fn_zero {α : Type u_1}  :
0 = 0
@[simp]
theorem measure_theory.finite_measure.coe_fn_add {α : Type u_1} (μ ν : measure_theory.finite_measure α) :
+ ν) = μ + ν
@[simp]
theorem measure_theory.finite_measure.coe_fn_smul {α : Type u_1} (c : ℝ≥0)  :
(c μ) = c μ
@[instance]
Equations

Coercion is an add_monoid_hom.

Equations
@[instance]
def measure_theory.finite_measure.module {α : Type u_1}  :
Equations
def measure_theory.probability_measure (α : Type u_1)  :
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
@[instance]
Equations
@[instance]

A probability measure can be interpreted as a measure.

Equations
@[instance]
def measure_theory.probability_measure.has_coe_to_fun {α : Type u_1}  :
(λ (_x : , set αℝ≥0)
Equations
@[instance]
@[simp]
@[simp]
theorem measure_theory.probability_measure.coe_fn_univ {α : Type u_1}  :
= 1

A probability measure can be interpreted as a finite measure.

Equations