Weak convergence from convergence of moments

The method of moments on the real line: if probability measures μᵢ on ℝ have finite moments of every order and ∫ xⁿ dμᵢ → ∫ xⁿ dμ for every n, where the limit μ is concentrated on a compact set, then μᵢ → μ weakly. The approximating measures need not be compactly supported, let alone supported in one common compact set. This is how a limit theorem proved by computing moments, such as the free central limit theorem or the moment convergence of a random-matrix ensemble, is turned into weak convergence of the corresponding laws.

Main results

• TauCeti.tendsto_integral_eval_of_tendsto_integral_pow — convergence of all moments gives convergence of the integral of every real polynomial.
• MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_integral_pow — the method of moments: moment convergence to a compactly supported limit implies weak convergence.

Implementation notes

The proof does not go through Prokhorov's theorem. Let |x| ≤ R on the support of μ, put M = R + 1, and fix a bounded continuous f with |f| ≤ C. By the Weierstrass approximation theorem there is a polynomial p with |f - p| < δ on [-M, M]. Outside [-M, M] the Markov-type bound 1 ≤ x²ⁿ / M²ⁿ and the inequality |p| ≤ t p² + 1 / (4t) give, for every x, |f x - p x| ≤ q x := δ + t p(x)² + (C + 1 / (4t)) x²ⁿ / M²ⁿ, with the polynomial q of the same shape for all i. Since ∫ q dμᵢ → ∫ q dμ ≤ δ + t (C + δ)² + (C + 1 / (4t)) (R / M)²ⁿ, the choice of a small t and then a large n makes ∫ |f - p| dμᵢ eventually small. The higher moments thus provide both the tightness and the uniform integrability of p that the standard argument through subsequential limits requires.

References

• P. Billingsley, Probability and Measure, 3rd ed., Wiley (1995), Theorem 30.2.

theorem TauCeti.tendsto_integral_eval_of_tendsto_integral_pow {ι : Type u_1} {l : Filter ι} {μs : ι → MeasureTheory.Measure ℝ} {μ : MeasureTheory.Measure ℝ} (hμs : ∀ (n : ℕ), ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (μs i)) (hμ : ∀ (n : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) μ) (h : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), x ^ n ∂μs i) l (nhds (∫ (x : ℝ), x ^ n ∂μ))) (p : Polynomial ℝ) : Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), Polynomial.eval x p ∂μs i) l (nhds (∫ (x : ℝ), Polynomial.eval x p ∂μ))

If every moment ∫ xⁿ dμᵢ converges to ∫ xⁿ dμ, then so does the integral of every real polynomial. The moments must be genuine: each monomial is assumed integrable against μ and, eventually, against μᵢ.

theorem MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_integral_pow {ι : Type u_1} {l : Filter ι} {μs : ι → ProbabilityMeasure ℝ} {μ : ProbabilityMeasure ℝ} {K : Set ℝ} (hK : IsCompact K) (hμK : ↑μ Kᶜ = 0) (hμs : ∀ (n : ℕ), ∀ᶠ (i : ι) in l, Integrable (fun (x : ℝ) => x ^ n) ↑(μs i)) (h : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => ∫ (x : ℝ), x ^ n ∂↑(μs i)) l (nhds (∫ (x : ℝ), x ^ n ∂↑μ))) : Filter.Tendsto μs l (nhds μ)

The method of moments. Let μᵢ and μ be probability measures on ℝ such that μ is concentrated on a compact set, every moment of μᵢ is eventually finite, and ∫ xⁿ dμᵢ → ∫ xⁿ dμ for every n. Then μᵢ → μ weakly.