mathlib documentation

measure_theory.measure.finite_measure_weak_convergence

Weak convergence of (finite) measures #

This file defines 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

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

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 α) :
+ ν) = μ + ν

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

The topology of weak convergence on finite_measures α is inherited (induced) from the weak-* topology on weak_dual ℝ≥0 (α →ᵇ ℝ≥0) via the function finite_measures.to_weak_dual_bcnn.

Equations
theorem measure_theory.finite_measure.tendsto_lintegral_nn_filter_of_le_const {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {ι : Type u_2} {L : filter ι} [L.is_countably_generated] (μ : measure_theory.finite_measure α) {fs : ι → bounded_continuous_function α nnreal} {c : nnreal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (a : α) ∂μ, (fs i) a c) {f : α → nnreal} (fs_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (i : ι), (fs i) a) L (nhds (f a))) :
filter.tendsto (λ (i : ι), ∫⁻ (a : α), ((fs i) a) μ) L (nhds (∫⁻ (a : α), (f a) μ))

A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes:

  • the functions tend to a limit along a countably generated filter;
  • the limit is in the almost everywhere sense;
  • boundedness holds almost everywhere;
  • integration is lintegral, i.e., the functions and their integrals are ℝ≥0∞-valued.
theorem measure_theory.finite_measure.tendsto_lintegral_nn_of_le_const {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] (μ : measure_theory.finite_measure α) {fs : bounded_continuous_function α nnreal} {c : nnreal} (fs_le_const : ∀ (n : ) (a : α), (fs n) a c) {f : α → nnreal} (fs_lim : ∀ (a : α), filter.tendsto (λ (n : ), (fs n) a) filter.at_top (nhds (f a))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), ((fs n) a) μ) filter.at_top (nhds (∫⁻ (a : α), (f a) μ))

A bounded convergence theorem for a finite measure: If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and tend pointwise to a limit, then their integrals (lintegral) against the finite measure tend to the integral of the limit.

A related result with more general assumptions is tendsto_lintegral_nn_filter_of_le_const.

theorem measure_theory.finite_measure.tendsto_test_against_nn_filter_of_le_const {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {ι : Type u_2} {L : filter ι} [L.is_countably_generated] {μ : measure_theory.finite_measure α} {fs : ι → bounded_continuous_function α nnreal} {c : nnreal} (fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (a : α) ∂μ, (fs i) a c) {f : bounded_continuous_function α nnreal} (fs_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (i : ι), (fs i) a) L (nhds (f a))) :
filter.tendsto (λ (i : ι), μ.test_against_nn (fs i)) L (nhds (μ.test_against_nn f))

A bounded convergence theorem for a finite measure: If bounded continuous non-negative functions are uniformly bounded by a constant and tend to a limit, then their integrals against the finite measure tend to the integral of the limit. This formulation assumes:

  • the functions tend to a limit along a countably generated filter;
  • the limit is in the almost everywhere sense;
  • boundedness holds almost everywhere;
  • integration is the pairing against non-negative continuous test functions (test_against_nn).

A related result using lintegral for integration is tendsto_lintegral_nn_filter_of_le_const.

theorem measure_theory.finite_measure.tendsto_test_against_nn_of_le_const {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {μ : measure_theory.finite_measure α} {fs : bounded_continuous_function α nnreal} {c : nnreal} (fs_le_const : ∀ (n : ) (a : α), (fs n) a c) {f : bounded_continuous_function α nnreal} (fs_lim : ∀ (a : α), filter.tendsto (λ (n : ), (fs n) a) filter.at_top (nhds (f a))) :

A bounded convergence theorem for a finite measure: If a sequence of bounded continuous non-negative functions are uniformly bounded by a constant and tend pointwise to a limit, then their integrals (test_against_nn) against the finite measure tend to the integral of the limit.

Related results:

  • tendsto_test_against_nn_filter_of_le_const: more general assumptions
  • tendsto_lintegral_nn_of_le_const: using lintegral for integration.
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
Instances for measure_theory.probability_measure

A probability measure can be interpreted as a finite measure.

Equations
@[protected, instance]

The topology of weak convergence on probability_measures α. This is inherited (induced) from the weak-* topology on weak_dual ℝ≥0 (α →ᵇ ℝ≥0) via the function probability_measures.to_weak_dual_bcnn.

Equations

The usual definition of weak convergence of probability measures is given in terms of sequences of probability measures: it is the requirement that the integrals of all continuous bounded functions against members of the sequence converge. This version is a characterization using nonnegative bounded continuous functions.

theorem measure_theory.measure_of_cont_bdd_of_tendsto_filter_indicator {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} [L.is_countably_generated] [topological_space α] [opens_measurable_space α] (μ : measure_theory.finite_measure α) {c : nnreal} {E : set α} (E_mble : measurable_set E) (fs : ι → bounded_continuous_function α nnreal) (fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (a : α) ∂μ, (fs i) a c) (fs_lim : ∀ᵐ (a : α) ∂μ, filter.tendsto (λ (i : ι), (fs i) a) L (nhds (E.indicator (λ (x : α), 1) a))) :
filter.tendsto (λ (n : ι), ∫⁻ (a : α), ((fs n) a) μ) L (nhds (μ E))

If bounded continuous functions tend to the indicator of a measurable set and are uniformly bounded, then their integrals against a finite measure tend to the measure of the set. This formulation assumes:

  • the functions tend to a limit along a countably generated filter;
  • the limit is in the almost everywhere sense;
  • boundedness holds almost everywhere.
theorem measure_theory.measure_of_cont_bdd_of_tendsto_indicator {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] (μ : measure_theory.finite_measure α) {c : nnreal} {E : set α} (E_mble : measurable_set E) (fs : bounded_continuous_function α nnreal) (fs_bdd : ∀ (n : ) (a : α), (fs n) a c) (fs_lim : filter.tendsto (λ (n : ), (fs n)) filter.at_top (nhds (E.indicator (λ (x : α), 1)))) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), ((fs n) a) μ) filter.at_top (nhds (μ E))

If a sequence of bounded continuous functions tends to the indicator of a measurable set and the functions are uniformly bounded, then their integrals against a finite measure tend to the measure of the set.

A similar result with more general assumptions is measure_of_cont_bdd_of_tendsto_filter_indicator.

theorem measure_theory.tendsto_lintegral_thickened_indicator_of_is_closed {α : Type u_1} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α] (μ : measure_theory.finite_measure α) {F : set α} (F_closed : is_closed F) {δs : } (δs_pos : ∀ (n : ), 0 < δs n) (δs_lim : filter.tendsto δs filter.at_top (nhds 0)) :

The integrals of thickenined indicators of a closed set against a finite measure tend to the measure of the closed set if the thickening radii tend to zero.

theorem measure_theory.finite_measure.limsup_measure_closed_le_of_tendsto {α : Type u_1} {ι : Type u_2} {L : filter ι} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α] {μ : measure_theory.finite_measure α} {μs : ι → measure_theory.finite_measure α} (μs_lim : filter.tendsto μs L (nhds μ)) {F : set α} (F_closed : is_closed F) :
L.limsup (λ (i : ι), (μs i) F) μ F

One implication of the portmanteau theorem: Weak convergence of finite measures implies that the limsup of the measures of any closed set is at most the measure of the closed set under the limit measure.