Integrals of unbounded functions along weakly convergent finite measures

Weak convergence μᵢ ⇀ μ of finite measures is defined by convergence of the integrals of bounded continuous functions. For an unbounded continuous function g : Ω → ℝ≥0 the integrals ∫⁻ g ∂μᵢ need not converge to ∫⁻ g ∂μ: mass escaping to the region where g is large can carry a non-vanishing share of the integral. This file proves that this is the only obstruction. The integrals converge exactly when the tails of g are uniformly integrable along the family: for every ε > 0 there is a level R such that eventually ∫⁻ x in {x | R ≤ g x}, g x ∂μᵢ ≤ ε.

This is the measure-theoretic core of the characterization of convergence in the p-Wasserstein distance by weak convergence together with convergence of p-moments, where g is the p-th power of the distance to a basepoint. Everything is stated for finite measures; probability measures are the special case reached through MeasureTheory.ProbabilityMeasure.toFiniteMeasure.

Both directions compare g with its truncations min g R, which are bounded continuous and hence have converging integrals, and use that g - R and the tail g on {x | 2 R ≤ g x} control each other. No metric structure on Ω and no finiteness of ∫⁻ g ∂μ is needed for the sufficiency of the tail condition; the necessity needs ∫⁻ g ∂μ ≠ ∞.

Main statements

• TauCeti.tendsto_lintegral_of_forall_exists_setLIntegral_le — uniformly integrable tails along a weakly convergent family give convergence of the integrals;
• TauCeti.tendsto_lintegral_of_sq_bound — an eventual uniform second-moment bound gives convergence of the integrals;
• TauCeti.exists_setLIntegral_le_of_tendsto_lintegral — conversely, convergence of the integrals to a finite limit gives uniformly integrable tails;
• TauCeti.tendsto_lintegral_iff_forall_exists_setLIntegral_le — the resulting equivalence.

References

• P. Billingsley, Convergence of Probability Measures, 2nd edition, Wiley 1999, Theorems 3.5 and 3.6, stated there for real random variables converging in distribution.
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Definition 6.8, where this tail condition defines weak convergence in P_p.

theorem TauCeti.tendsto_lintegral_of_forall_exists_setLIntegral_le {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {g : Ω → NNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (hg : Continuous g) (h : Filter.Tendsto μs L (nhds μ)) (htail : ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (x : Ω) in {x : Ω | R ≤ g x}, ↑(g x) ∂↑(μs i) ≤ ε) : Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) L (nhds (∫⁻ (x : Ω), ↑(g x) ∂↑μ))

Uniformly integrable tails give convergence of integrals. Along a weakly convergent family of finite measures, the integrals of a continuous function g : Ω → ℝ≥0 converge as soon as its tails are uniformly small: for every ε > 0 there is a level R beyond which eventually the integral of g is at most ε.

theorem TauCeti.exists_setLIntegral_le_of_tendsto_lintegral {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {g : Ω → NNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (hg : Continuous g) (h : Filter.Tendsto μs L (nhds μ)) (hμ : ∫⁻ (x : Ω), ↑(g x) ∂↑μ ≠ ⊤) (hlim : Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) L (nhds (∫⁻ (x : Ω), ↑(g x) ∂↑μ))) {ε : ENNReal} (hε : 0 < ε) : ∃ (R : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (x : Ω) in {x : Ω | R ≤ g x}, ↑(g x) ∂↑(μs i) ≤ ε

Convergence of integrals gives uniformly integrable tails. If a continuous function g : Ω → ℝ≥0 has finite integral against the limit of a weakly convergent family of finite measures, and its integrals converge along the family, then its tails are uniformly small: for every ε > 0 there is a level R beyond which eventually the integral of g is at most ε.

theorem TauCeti.tendsto_lintegral_iff_forall_exists_setLIntegral_le {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {g : Ω → NNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (hg : Continuous g) (h : Filter.Tendsto μs L (nhds μ)) (hμ : ∫⁻ (x : Ω), ↑(g x) ∂↑μ ≠ ⊤) : Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) L (nhds (∫⁻ (x : Ω), ↑(g x) ∂↑μ)) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (R : NNReal), ∀ᶠ (i : γ) in L, ∫⁻ (x : Ω) in {x : Ω | R ≤ g x}, ↑(g x) ∂↑(μs i) ≤ ε

Convergence of integrals of an unbounded function along weak convergence. Along a weakly convergent family of finite measures, the integrals of a continuous function g : Ω → ℝ≥0 with finite integral against the limit converge to that integral exactly when the tails of g are uniformly small along the family.

theorem TauCeti.tendsto_lintegral_of_sq_bound {Ω : Type u_1} [MeasurableSpace Ω] [TopologicalSpace Ω] [OpensMeasurableSpace Ω] {g : Ω → NNReal} {γ : Type u_2} {L : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω} (hg : Continuous g) (h : Filter.Tendsto μs L (nhds μ)) {C : NNReal} (hC : ∀ᶠ (i : γ) in L, ∫⁻ (x : Ω), ↑(g x) ^ 2 ∂↑(μs i) ≤ ↑C) : Filter.Tendsto (fun (i : γ) => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) L (nhds (∫⁻ (x : Ω), ↑(g x) ∂↑μ))

A uniform second-moment bound for a continuous nonnegative function gives convergence of its integrals along weakly convergent finite measures.