Characterizations of weak convergence of finite measures and probability measures

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

The topologies of weak convergence on the types of finite measures and probability measures are already defined in their corresponding files; no substantial new definitions are introduced here.

Main results

The main result will be the portmanteau theorem providing various characterizations of the weak convergence of measures (probability measures or finite measures). Given measures μs and μ on a topological space Ω, the conditions that will be proven equivalent (under quite general hypotheses) are:

(T) The measures μs tend to the measure μ weakly. (C) For any closed set F, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F). (O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G). (B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B).

The separate implications are:

• MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto is the implication (T) → (C).
• MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge is the equivalence (C) ↔ (O).
• MeasureTheory.tendsto_measure_of_null_frontier is the implication (O) → (B).
• MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure is the implication (B) → (C).
• MeasureTheory.tendsto_of_forall_isOpen_le_liminf gives the implication (O) → (T) for any sequence of Borel probability measures.

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 more general assumptions than in the usual statement of portmanteau theorem. The full portmanteau theorem, however, is most convenient for probability measures on pseudo-emetrizable spaces with their Borel sigma algebras.

Some specific considerations on the assumptions in the different implications:

• MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto assumes PseudoEMetricSpace. The only reason is to have bounded continuous pointwise approximations to the indicator function of a closed set. Clearly for example metrizability or pseudo-emetrizability would be sufficient assumptions. The typeclass assumptions should be later adjusted in a way that takes into account use cases, but the proof will presumably remain essentially the same.
• Where formulations are currently only provided for probability measures, one can obtain the finite measure formulations using the characterization of convergence of finite measures by their total masses and their probability-normalized versions, i.e., by MeasureTheory.FiniteMeasure.tendsto_normalize_iff_tendsto.

References

• [Billingsley, Convergence of probability measures][billingsley1999]

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, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F); (O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G).

Either of these will later be shown to be equivalent to the weak convergence of the sequence of measures.

theorem MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : Filter.limsup (fun (i : ι) => ↑↑(μs i) E) L ≤ ↑↑μ E) : ↑↑μ Eᶜ ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) Eᶜ) L

Portmanteau theorem

theorem MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : Filter.limsup (fun (i : ι) => ↑↑(μs i) Eᶜ) L ≤ ↑↑μ Eᶜ) : ↑↑μ E ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) E) L

theorem MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : ↑↑μ E ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) E) L) : Filter.limsup (fun (i : ι) => ↑↑(μs i) Eᶜ) L ≤ ↑↑μ Eᶜ

theorem MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] {E : Set Ω} (E_mble : MeasurableSet E) (h : ↑↑μ Eᶜ ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) Eᶜ) L) : Filter.limsup (fun (i : ι) => ↑↑(μs i) E) L ≤ ↑↑μ E

theorem MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] : (∀ (F : Set Ω), IsClosed F → Filter.limsup (fun (i : ι) => ↑↑(μs i) F) L ≤ ↑↑μ F) ↔ ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) G) L

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, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F); (O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G).

implies that

(B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B).

theorem MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} {E₀ : Set Ω} {E : Set Ω} {E₁ : Set Ω} (E₀_subset : E₀ ⊆ E) (subset_E₁ : E ⊆ E₁) (nulldiff : ↑↑μ (E₁ \ E₀) = 0) (h_E₀ : ↑↑μ E₀ ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) E₀) L) (h_E₁ : Filter.limsup (fun (i : ι) => ↑↑(μs i) E₁) L ≤ ↑↑μ E₁) : Filter.Tendsto (fun (i : ι) => ↑↑(μs i) E) L (nhds (↑↑μ E))

theorem MeasureTheory.tendsto_measure_of_null_frontier {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} {μs : ι → MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h_opens : ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) G) L) {E : Set Ω} (E_nullbdry : ↑↑μ (frontier E) = 0) : Filter.Tendsto (fun (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

(T) The measures μs tend to the measure μ weakly

implies

(C) For any closed set F, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F).

Combining with a earlier proven implications, we get that (T) implies also both

(O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G); (B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B).

theorem MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [TopologicalSpace Ω] [HasOuterApproxClosed Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {μs : ι → MeasureTheory.FiniteMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {F : Set Ω} (F_closed : IsClosed F) : Filter.limsup (fun (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.

theorem MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {F : Set Ω} (F_closed : IsClosed F) : Filter.limsup (fun (i : ι) => ↑↑↑(μs i) F) L ≤ ↑↑↑μ 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 MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {G : Set Ω} (G_open : IsOpen G) : ↑↑↑μ G ≤ Filter.liminf (fun (i : ι) => ↑↑↑(μs i) G) L

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 MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto' {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {E : Set Ω} (E_nullbdry : ↑↑↑μ (frontier E) = 0) : Filter.Tendsto (fun (i : ι) => ↑↑↑(μs i) E) L (nhds (↑↑↑μ E))

theorem MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ι → MeasureTheory.ProbabilityMeasure Ω} (μs_lim : Filter.Tendsto μs L (nhds μ)) {E : Set Ω} (E_nullbdry : (fun (s : Set Ω) => ENNReal.toNNReal (↑↑↑μ s)) (frontier E) = 0) : Filter.Tendsto (fun (i : ι) => (fun (s : Set Ω) => ENNReal.toNNReal (↑↑↑(μs i) s)) E) L (nhds ((fun (s : Set Ω) => ENNReal.toNNReal (↑↑↑μ s)) 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 MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'.

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

In this section we prove, under the assumption that the underlying topological space Ω is pseudo-emetrizable, that

(B) For any Borel set B whose boundary carries no mass under μ, i.e. μ(∂B) = 0, the measures of B under μs tend to the measure of B under μ, i.e., limᵢ μsᵢ(B) = μ(B)

implies

(C) For any closed set F, the limsup of the measures of F under μs is at most the measure of F under μ, i.e., limsupᵢ μsᵢ(F) ≤ μ(F).

Combining with a earlier proven implications, we get that (B) implies also

(O) For any open set G, the liminf of the measures of G under μs is at least the measure of G under μ, i.e., μ(G) ≤ liminfᵢ μsᵢ(G).

theorem MeasureTheory.exists_null_frontier_thickening {Ω : Type u_1} [PseudoEMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite μ] (s : Set Ω) {a : ℝ} {b : ℝ} (hab : a < b) : ∃ r ∈ Set.Ioo a b, ↑↑μ (frontier (Metric.thickening r s)) = 0

theorem MeasureTheory.exists_null_frontiers_thickening {Ω : Type u_1} [PseudoEMetricSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFinite μ] (s : Set Ω) : ∃ (rs : ℕ → ℝ), Filter.Tendsto rs Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ ↑↑μ (frontier (Metric.thickening (rs n) s)) = 0

theorem MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure {Ω : Type u_2} {ι : Type u_3} {L : Filter ι} [Filter.NeBot L] [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω} (h : ∀ {E : Set Ω}, MeasurableSet E → ↑↑μ (frontier E) = 0 → Filter.Tendsto (fun (i : ι) => ↑↑(μs i) E) L (nhds (↑↑μ E))) (F : Set Ω) (F_closed : IsClosed F) : Filter.limsup (fun (i : ι) => ↑↑(μs i) F) L ≤ ↑↑μ F

One implication of the portmanteau theorem: Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E), then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F).

theorem MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure {Ω : Type u_2} {ι : Type u_3} {L : Filter ι} [Filter.NeBot L] [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ {E : Set Ω}, MeasurableSet E → ↑↑μ (frontier E) = 0 → Filter.Tendsto (fun (i : ι) => ↑↑(μs i) E) L (nhds (↑↑μ E))) (G : Set Ω) (G_open : IsOpen G) : ↑↑μ G ≤ Filter.liminf (fun (i : ι) => ↑↑(μs i) G) L

One implication of the portmanteau theorem: Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E), then for all open sets G we have the limsup condition μ(G) ≤ liminf μsᵢ(G).

Portmanteau implication: liminf condition for open sets implies weak convergence

In this section we prove for a sequence (μsₙ)ₙ Borel probability measures that

(O) For any open set G, the liminf of the measures of G under μsₙ is at least the measure of G under μ, i.e., μ(G) ≤ liminfₙ μsₙ(G).

implies

(T) The measures μsₙ converge weakly to the measure μ.

theorem MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {μs : ℕ → MeasureTheory.Measure Ω} {f : Ω → ℝ} (f_cont : Continuous f) (f_nn : 0 ≤ f) (h_opens : ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun (i : ℕ) => ↑↑(μs i) G) Filter.atTop) : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ Filter.liminf (fun (i : ℕ) => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) Filter.atTop

theorem MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {μs : ℕ → MeasureTheory.Measure Ω} [∀ (i : ℕ), MeasureTheory.IsProbabilityMeasure (μs i)] {f : BoundedContinuousFunction Ω ℝ} (f_nn : 0 ≤ f) (h_opens : ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ Filter.liminf (fun (i : ℕ) => ↑↑(μs i) G) Filter.atTop) : ∫ (x : Ω), f x ∂μ ≤ Filter.liminf (fun (i : ℕ) => ∫ (x : Ω), f x ∂μs i) Filter.atTop

theorem MeasureTheory.tendsto_integral_of_forall_integral_le_liminf_integral {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {μs : ι → MeasureTheory.Measure Ω} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μs i)] (h : ∀ (f : BoundedContinuousFunction Ω ℝ), 0 ≤ f → ∫ (x : Ω), f x ∂μ ≤ Filter.liminf (fun (i : ι) => ∫ (x : Ω), f x ∂μs i) L) (f : BoundedContinuousFunction Ω ℝ) : Filter.Tendsto (fun (i : ι) => ∫ (x : Ω), f x ∂μs i) L (nhds (∫ (x : Ω), f x ∂μ))

theorem MeasureTheory.tendsto_of_forall_isOpen_le_liminf {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.ProbabilityMeasure Ω} {μs : ℕ → MeasureTheory.ProbabilityMeasure Ω} (h_opens : ∀ (G : Set Ω), IsOpen G → (fun (s : Set Ω) => ENNReal.toNNReal (↑↑↑μ s)) G ≤ Filter.liminf (fun (i : ℕ) => (fun (s : Set Ω) => ENNReal.toNNReal (↑↑↑(μs i) s)) G) Filter.atTop) : Filter.Tendsto (fun (i : ℕ) => μs i) Filter.atTop (nhds μ)

One implication of the portmanteau theorem: If for all open sets G we have the liminf condition μ(G) ≤ liminf μsₙ(G), then the measures μsₙ converge weakly to the measure μ.