mathlib3 documentation

measure_theory.measure.portmanteau

Characterizations of weak convergence of finite measures and probability measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file will provide portmanteau characterizations of the weak convergence of finite measures and of probability measures, i.e., the standard characterizations of convergence in distribution.

Main definitions #

This file does not introduce substantial new definitions: the topologies of weak convergence on the types of finite measures and probability measures are already defined in their corresponding files.

Main results #

The main result will be the portmanteau theorem providing various characterizations of the weak convergence of measures. The separate implications are:

TODO:

Implementation notes #

Many of the characterizations of weak convergence hold for finite measures and are proven in that generality and then specialized to probability measures. Some implications hold with slightly weaker assumptions than usually stated. The full portmanteau theorem, however, is most convenient for probability measures on metrizable spaces with their Borel sigmas.

Some specific considerations on the assumptions in the different implications:

References #

Tags #

weak convergence of measures, convergence in distribution, convergence in law, finite measure, probability measure

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 : filter.limsup (λ (i : ι), (μs i) E) L μ E) :
μ E filter.liminf (λ (i : ι), (μs i) E) L
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 : filter.limsup (λ (i : ι), (μs i) E) L μ E) :
μ E filter.liminf (λ (i : ι), (μs i) E) L
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 filter.liminf (λ (i : ι), (μs i) E) L) :
filter.limsup (λ (i : ι), (μs i) E) L μ 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 filter.liminf (λ (i : ι), (μs i) E) L) :
filter.limsup (λ (i : ι), (μs i) E) L μ E

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₀ filter.liminf (λ (i : ι), (μs i) E₀) L) (h_E₁ : filter.limsup (λ (i : ι), (μs i) E₁) L μ 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 filter.liminf (λ (i : ι), (μs i) G) L) {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, ∀ᵐ (ω : Ω) μ, (fs i) ω c) (fs_lim : ∀ᵐ (ω : Ω) μ, filter.tendsto (λ (i : ι), (fs i) ω) L (nhds (E.indicator (λ (x : Ω), 1) ω))) :
filter.tendsto (λ (n : ι), ∫⁻ (ω : Ω), ((fs n) ω) μ) 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 : ) (ω : Ω), (fs n) ω c) (fs_lim : filter.tendsto (λ (n : ), (fs n)) filter.at_top (nhds (E.indicator (λ (x : Ω), 1)))) :
filter.tendsto (λ (n : ), ∫⁻ (ω : Ω), ((fs n) ω) μ) 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.

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) :
filter.limsup (λ (i : ι), (μs i) F) L μ 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.

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.

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))

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'.

Portmanteau implication: limit condition for Borel sets implies limsup for closed sets #

TODO: The proof of the implication is not yet here. Add it.