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 α;
• to_weak_dual_bounded_continuous_nnreal : 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 will be used for the definition of the topology of weak convergence.

TODO:

• Define the topologies on the above types.

Main results #

• Finite measures μ on α give rise to continuous linear functionals on the space of bounded continuous nonnegative functions on α via integration: to_weak_dual_of_bounded_continuous_nnreal : finite_measure α → (weak_dual ℝ≥0 (α →ᵇ ℝ≥0)).

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
@[protected, instance]

A finite measure can be interpreted as a measure.

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

Coercion is an add_monoid_hom.

Equations
@[protected, instance]
noncomputable def measure_theory.finite_measure.module {α : Type u_1}  :
Equations
noncomputable def measure_theory.finite_measure.test_against_nn {α : Type u_1} (f : α →ᵇ ℝ≥0) :

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
@[simp]
theorem measure_theory.finite_measure.test_against_nn_mono {α : Type u_1} {f g : α →ᵇ ℝ≥0} (f_le_g : f g) :
theorem measure_theory.finite_measure.test_against_nn_add {α : Type u_1} (f₁ f₂ : α →ᵇ ℝ≥0) :
μ.test_against_nn (f₁ + f₂) = μ.test_against_nn f₁ + μ.test_against_nn f₂

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)  :
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
@[protected, instance]
noncomputable def measure_theory.probability_measure.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected, instance]

A probability measure can be interpreted as a measure.

Equations
@[protected, instance]
def measure_theory.probability_measure.has_coe_to_fun {α : Type u_1}  :
(λ (_x : , set αℝ≥0)
Equations
@[protected, 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
noncomputable def measure_theory.probability_measure.test_against_nn {α : Type u_1} (f : α →ᵇ ℝ≥0) :

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
@[simp]
theorem measure_theory.probability_measure.test_against_nn_mono {α : Type u_1} {f g : α →ᵇ ℝ≥0} (f_le_g : f g) :

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

Equations