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 measure_theory.finite_measure α to weak_dual ℝ≥0 (α →ᵇ ℝ≥0), inheriting the topology from the latter.

The current implementation of measure_theory.finite_measure α and measure_theory.probability_measure α is directly as subtypes of measure_theory.measure α, and the coercion to a function is the composition ennreal.to_nnreal and the coercion to function of measure_theory.measure α. Another alternative would be to use a bijection with measure_theory.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:

Potential drawbacks of the vector measure alternative:

References #

Tags #

weak convergence of measures, finite measure, probability measure

Finite measures #

In this section we define the Type of finite_measure α, when α is a measurable space. Finite measures on α are a module over ℝ≥0.

If α is moreover a topological space and the sigma algebra on α is finer than the Borel sigma algebra (i.e. [opens_measurable_space α]), then finite_measure α is equipped with the topology of weak convergence of measures. This is implemented by defining a pairing of finite measures μ on α with continuous bounded nonnegative functions f : α →ᵇ ℝ≥0 via integration, and using the associated weak topology (essentially the weak-star topology on the dual of α →ᵇ ℝ≥0).

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.zero.mass {α : Type u_1} [measurable_space α] :
0.mass = 0
@[simp]
@[ext]
theorem measure_theory.finite_measure.extensionality {α : Type u_1} [measurable_space α] (μ ν : measure_theory.finite_measure α) (h : ∀ (s : set α), measurable_set sμ s = ν s) :
μ = ν
@[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 measure_theory.finite_measure.test_against_nn, i.e., integration.

Equations

The total mass of a finite measure depends continuously on the measure.

theorem filter.tendsto.mass {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} {μ : measure_theory.finite_measure α} (h : filter.tendsto μs F (nhds μ)) :
filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass)

Convergence of finite measures implies the convergence of their total masses.

theorem measure_theory.finite_measure.tendsto_zero_test_against_nn_of_tendsto_zero_mass {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds 0)) (f : bounded_continuous_function α nnreal) :
filter.tendsto (λ (i : γ), (μs i).test_against_nn f) F (nhds 0)

If the total masses of finite measures tend to zero, then the measures tend to zero. This formulation concerns the associated functionals on bounded continuous nonnegative test functions. See finite_measure.tendsto_zero_of_tendsto_zero_mass for a formulation stating the weak convergence of measures.

theorem measure_theory.finite_measure.tendsto_zero_of_tendsto_zero_mass {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds 0)) :

If the total masses of finite measures tend to zero, then the measures tend to zero.

theorem measure_theory.finite_measure.tendsto_iff_forall_lintegral_tendsto {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} {μ : measure_theory.finite_measure α} :
filter.tendsto μs F (nhds μ) ∀ (f : bounded_continuous_function α nnreal), filter.tendsto (λ (i : γ), ∫⁻ (x : α), (f x) (μs i)) F (nhds (∫⁻ (x : α), (f x) μ))

A characterization of weak convergence in terms of integrals of bounded continuous nonnegative functions.

Bounded convergence results for finite measures #

This section is about bounded convergence theorems for finite measures.

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.measure α) [measure_theory.is_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 measure_theory.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 (measure_theory.lintegral) against the finite measure tend to the integral of the limit.

A related result with more general assumptions is measure_theory.finite_measure.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 (measure_theory.finite_measure.test_against_nn).

A related result using measure_theory.lintegral for integration is measure_theory.finite_measure.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 (measure_theory.finite_measure.test_against_nn) against the finite measure tend to the integral of the limit.

Related results:

Weak convergence of finite measures with bounded continuous real-valued functions #

In this section we characterize the weak convergence of finite measures by the usual (defining) condition that the integrals of all bounded continuous real-valued functions converge.

theorem measure_theory.finite_measure.tendsto_of_forall_integral_tendsto {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} {μ : measure_theory.finite_measure α} (h : ∀ (f : bounded_continuous_function α ), filter.tendsto (λ (i : γ), (x : α), f x (μs i)) F (nhds ( (x : α), f x μ))) :
filter.tendsto μs F (nhds μ)
theorem measure_theory.finite_measure.tendsto_iff_forall_integral_tendsto {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} {μ : measure_theory.finite_measure α} :
filter.tendsto μs F (nhds μ) ∀ (f : bounded_continuous_function α ), filter.tendsto (λ (i : γ), (x : α), f x (μs i)) F (nhds ( (x : α), f x μ))

A characterization of weak convergence in terms of integrals of bounded continuous real-valued functions.

Probability measures #

In this section we define the type of probability measures on a measurable space α, denoted by measure_theory.probability_measure α. TODO: Probability measures form a convex space.

If α is moreover a topological space and the sigma algebra on α is finer than the Borel sigma algebra (i.e. [opens_measurable_space α]), then measure_theory.probability_measure α is equipped with the topology of weak convergence of measures. Since every probability measure is a finite measure, this is implemented as the induced topology from the coercion measure_theory.probability_measure.to_finite_measure.

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
@[ext]
theorem measure_theory.probability_measure.extensionality {α : Type u_1} [measurable_space α] (μ ν : measure_theory.probability_measure α) (h : ∀ (s : set α), measurable_set sμ s = ν s) :
μ = ν

A characterization of weak convergence of probability measures by the condition that the integrals of every continuous bounded nonnegative function converge to the integral of the function against the limit measure.

The characterization of weak convergence of probability measures by the usual (defining) condition that the integrals of every continuous bounded function converge to the integral of the function against the limit measure.

Normalization of finite measures to probability measures #

This section is about normalizing finite measures to probability measures.

The weak convergence of finite measures to nonzero limit measures is characterized by the convergence of the total mass and the convergence of the normalized probability measures.

Normalize a finite measure so that it becomes a probability measure, i.e., divide by the total mass.

Equations
@[simp]
theorem measure_theory.finite_measure.normalize_eq_of_nonzero {α : Type u_1} [nonempty α] {m0 : measurable_space α} (μ : measure_theory.finite_measure α) (nonzero : μ 0) (s : set α) :
(μ.normalize) s = (μ.mass)⁻¹ * μ s
theorem measure_theory.finite_measure.average_eq_integral_normalize {α : Type u_1} [nonempty α] {m0 : measurable_space α} (μ : measure_theory.finite_measure α) {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] (nonzero : μ 0) (f : α → E) :

Averaging with respect to a finite measure is the same as integraing against measure_theory.finite_measure.normalize.

theorem measure_theory.finite_measure.tendsto_test_against_nn_of_tendsto_normalize_test_against_nn_of_tendsto_mass {α : Type u_1} [nonempty α] {m0 : measurable_space α} {μ : measure_theory.finite_measure α} [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (μs_lim : filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize)) (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass)) (f : bounded_continuous_function α nnreal) :
filter.tendsto (λ (i : γ), (μs i).test_against_nn f) F (nhds (μ.test_against_nn f))
theorem measure_theory.finite_measure.tendsto_of_tendsto_normalize_test_against_nn_of_tendsto_mass {α : Type u_1} [nonempty α] {m0 : measurable_space α} {μ : measure_theory.finite_measure α} [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (μs_lim : filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize)) (mass_lim : filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass)) :
filter.tendsto μs F (nhds μ)

If the normalized versions of finite measures converge weakly and their total masses also converge, then the finite measures themselves converge weakly.

theorem measure_theory.finite_measure.tendsto_normalize_of_tendsto {α : Type u_1} [nonempty α] {m0 : measurable_space α} {μ : measure_theory.finite_measure α} [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (μs_lim : filter.tendsto μs F (nhds μ)) (nonzero : μ 0) :
filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize)

If finite measures themselves converge weakly to a nonzero limit measure, then their normalized versions also converge weakly.

theorem measure_theory.finite_measure.tendsto_normalize_iff_tendsto {α : Type u_1} [nonempty α] {m0 : measurable_space α} {μ : measure_theory.finite_measure α} [topological_space α] [opens_measurable_space α] {γ : Type u_2} {F : filter γ} {μs : γ → measure_theory.finite_measure α} (nonzero : μ 0) :
filter.tendsto (λ (i : γ), (μs i).normalize) F (nhds μ.normalize) filter.tendsto (λ (i : γ), (μs i).mass) F (nhds μ.mass) filter.tendsto μs F (nhds μ)

The weak convergence of finite measures to a nonzero limit can be characterized by the weak convergence of both their normalized versions (probability measures) and their total masses.

Portmanteau: limsup condition for closed sets iff liminf condition for open sets #

In this section we prove that for a sequence of Borel probability measures on a topological space and its candidate limit measure, the following two conditions are equivalent: (C) For any closed set F in α the limsup of the measures of F is at most the limit measure of F. (O) For any open set G in α the liminf of the measures of G is at least the limit measure of G. Either of these will later be shown to be equivalent to the weak convergence of the sequence of measures.

theorem measure_theory.le_measure_compl_liminf_of_limsup_measure_le {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] {E : set α} (E_mble : measurable_set E) (h : L.limsup (λ (i : ι), (μs i) E) μ E) :
μ E L.liminf (λ (i : ι), (μs i) E)
theorem measure_theory.le_measure_liminf_of_limsup_measure_compl_le {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] {E : set α} (E_mble : measurable_set E) (h : L.limsup (λ (i : ι), (μs i) E) μ E) :
μ E L.liminf (λ (i : ι), (μs i) E)
theorem measure_theory.limsup_measure_compl_le_of_le_liminf_measure {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] {E : set α} (E_mble : measurable_set E) (h : μ E L.liminf (λ (i : ι), (μs i) E)) :
L.limsup (λ (i : ι), (μs i) E) μ E
theorem measure_theory.limsup_measure_le_of_le_liminf_measure_compl {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] {E : set α} (E_mble : measurable_set E) (h : μ E L.liminf (λ (i : ι), (μs i) E)) :
L.limsup (λ (i : ι), (μs i) E) μ E
theorem measure_theory.limsup_measure_closed_le_iff_liminf_measure_open_ge {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] :
(∀ (F : set α), is_closed FL.limsup (λ (i : ι), (μs i) F) μ F) ∀ (G : set α), is_open Gμ G L.liminf (λ (i : ι), (μs i) G)

One pair of implications of the portmanteau theorem: For a sequence of Borel probability measures, the following two are equivalent:

(C) The limsup of the measures of any closed set is at most the measure of the closed set under a candidate limit measure.

(O) The liminf of the measures of any open set is at least the measure of the open set under a candidate limit measure.

Portmanteau: limit of measures of Borel sets whose boundary carries no mass in the limit #

In this section we prove that for a sequence of Borel probability measures on a topological space and its candidate limit measure, either of the following equivalent conditions: (C) For any closed set F in α the limsup of the measures of F is at most the limit measure of F (O) For any open set G in α the liminf of the measures of G is at least the limit measure of G implies that (B) For any Borel set E in α whose boundary ∂E carries no mass under the candidate limit measure, we have that the limit of measures of E is the measure of E under the candidate limit measure.

theorem measure_theory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le {α : Type u_1} [measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} {E₀ E E₁ : set α} (E₀_subset : E₀ E) (subset_E₁ : E E₁) (nulldiff : μ (E₁ \ E₀) = 0) (h_E₀ : μ E₀ L.liminf (λ (i : ι), (μs i) E₀)) (h_E₁ : L.limsup (λ (i : ι), (μs i) E₁) μ E₁) :
filter.tendsto (λ (i : ι), (μs i) E) L (nhds (μ E))
theorem measure_theory.tendsto_measure_of_null_frontier {α : Type u_1} [measurable_space α] [topological_space α] [opens_measurable_space α] {ι : Type u_2} {L : filter ι} {μ : measure_theory.measure α} {μs : ι → measure_theory.measure α} [measure_theory.is_probability_measure μ] [∀ (i : ι), measure_theory.is_probability_measure (μs i)] (h_opens : ∀ (G : set α), is_open Gμ G L.liminf (λ (i : ι), (μs i) G)) {E : set α} (E_nullbdry : μ (frontier E) = 0) :
filter.tendsto (λ (i : ι), (μs i) E) L (nhds (μ E))

One implication of the portmanteau theorem: For a sequence of Borel probability measures, if the liminf of the measures of any open set is at least the measure of the open set under a candidate limit measure, then for any set whose boundary carries no probability mass under the candidate limit measure, then its measures under the sequence converge to its measure under the candidate limit measure.

Portmanteau implication: weak convergence implies a limsup condition for closed sets #

In this section we prove, under the assumption that the underlying topological space α is pseudo-emetrizable, that the weak convergence of measures on measure_theory.finite_measure α implies that for any closed set F in α the limsup of the measures of F is at most the limit measure of F. This is one implication of the portmanteau theorem characterizing weak convergence of measures.

Combining with an earlier implication we also get that weak convergence implies that for any Borel set E in α whose boundary ∂E carries no mass under the limit measure, the limit of measures of E is the measure of E under the limit measure.

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.measure α) [measure_theory.is_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.measure α) [measure_theory.is_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_theory.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.measure α) [measure_theory.is_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)) :
filter.tendsto (λ (n : ), ∫⁻ (a : α), ((thickened_indicator _ F) a) μ) filter.at_top (nhds (μ F))

The integrals of thickened 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.

theorem measure_theory.probability_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.probability_measure α} {μs : ι → measure_theory.probability_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 probability measures implies that the limsup of the measures of any closed set is at most the measure of the closed set under the limit probability measure.

theorem measure_theory.probability_measure.le_liminf_measure_open_of_tendsto {α : Type u_1} {ι : Type u_2} {L : filter ι} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α] {μ : measure_theory.probability_measure α} {μs : ι → measure_theory.probability_measure α} (μs_lim : filter.tendsto μs L (nhds μ)) {G : set α} (G_open : is_open G) :
μ G L.liminf (λ (i : ι), (μs i) G)

One implication of the portmanteau theorem: Weak convergence of probability measures implies that the liminf of the measures of any open set is at least the measure of the open set under the limit probability measure.

theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto' {α : Type u_1} {ι : Type u_2} {L : filter ι} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α] {μ : measure_theory.probability_measure α} {μs : ι → measure_theory.probability_measure α} (μs_lim : filter.tendsto μs L (nhds μ)) {E : set α} (E_nullbdry : μ (frontier E) = 0) :
filter.tendsto (λ (i : ι), (μs i) E) L (nhds (μ E))
theorem measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto {α : Type u_1} {ι : Type u_2} {L : filter ι} [measurable_space α] [pseudo_emetric_space α] [opens_measurable_space α] {μ : measure_theory.probability_measure α} {μs : ι → measure_theory.probability_measure α} (μs_lim : filter.tendsto μs L (nhds μ)) {E : set α} (E_nullbdry : μ (frontier E) = 0) :
filter.tendsto (λ (i : ι), (μs i) E) L (nhds (μ E))

One implication of the portmanteau theorem: Weak convergence of probability measures implies that if the boundary of a Borel set carries no probability mass under the limit measure, then the limit of the measures of the set equals the measure of the set under the limit probability measure.

A version with coercions to ordinary ℝ≥0∞-valued measures is measure_theory.probability_measure.tendsto_measure_of_null_frontier_of_tendsto'.