Convergence of probability measures

Weak convergence and convergence in probability, tightness and Prokhorov's theorem, Helly selection, Skorokhod representation, the continuous mapping theorem, the Cramér–Wold device and total variation distance; specific limit laws go to the limit-theorem fields.

• Continuous mapping theorem
• Convergence in probability
• Helly's selection theorem
• Slutsky's theorem and the delta method
• Tightness of probability measures
• Total variation distance
• Weak convergence in the space of continuous functions

TheoremCramér–Wold device#✓fully proved

Let \(d\) be a natural number, let \((\Omega, \mu)\) and \((\Omega', \mu')\) be probability spaces, and let \(X_n : \Omega \to \mathbb{R}^d\) for \(n \in \mathbb{N}\) and \(Z : \Omega' \to \mathbb{R}^d\) be maps, where \(\mathbb{R}^d\) carries the Euclidean inner product. If for every \(t \in \mathbb{R}^d\) the real-valued maps \(\langle t, X_n \rangle\) converge in distribution to \(\langle t, Z \rangle\) as \(n \to \infty\), then \(X_n\) converges in distribution to \(Z\) as \(n \to \infty\).

Here convergence in distribution means that every \(X_n\) and the limit are almost everywhere measurable and their laws converge weakly as probability measures.

theorem cramer_wold_device
    {d : ℕ} {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'} [IsProbabilityMeasure μ']
    (X : ℕ → Ω → EuclideanSpace ℝ (Fin d)) (Z : Ω' → EuclideanSpace ℝ (Fin d))
    (h : ∀ t : EuclideanSpace ℝ (Fin d),
      TendstoInDistribution
        (fun n (ω : Ω) => @inner ℝ (EuclideanSpace ℝ (Fin d)) _ t (X n ω))
        Filter.atTop
        (fun ω' => @inner ℝ (EuclideanSpace ℝ (Fin d)) _ t (Z ω'))
        (fun _ => μ) μ') :
    TendstoInDistribution X Filter.atTop Z (fun _ => μ) μ'

Sources

• H. Cramér and H. Wold, "Some Theorems on Distribution Functions", Journal of the London Mathematical Society s1-11 (1936), 290–294, DOI 10.1112/jlms/s1-11.4.290.

TheoremProkhorov's theorem, sequential form on \(\mathbb{R}\)#✓fully proved

A sequence \((\mu_n)\) of probability measures on \(\mathbb{R}\) is tight if and only if every subsequence of \((\mu_n)\) has a further subsequence converging weakly to a probability measure on \(\mathbb{R}\).

theorem prokhorov_sequential (μ : ℕ → ProbabilityMeasure ℝ) :
    IsTightMeasureSet {((μ n : ProbabilityMeasure ℝ) : Measure ℝ) | n} ↔
      ∀ f : ℕ → ℕ, StrictMono f →
        ∃ g : ℕ → ℕ, StrictMono g ∧ ∃ ν : ProbabilityMeasure ℝ,
          Tendsto (μ ∘ f ∘ g) atTop (𝓝 ν)

TheoremSkorokhod representation theorem#✓fully proved

Let \(X\) be a Polish space with its Borel \(\sigma\)-algebra, let \((\mu_n)_{n \in \mathbb{N}}\) be a sequence of probability measures on \(X\), and let \(\mu\) be a probability measure on \(X\) such that \(\mu_n\) converges weakly to \(\mu\). Write \(\lambda\) for Lebesgue measure on \(\mathbb{R}\) restricted to \([0, 1]\). Then there exist measurable maps \(Y_n : \mathbb{R} \to X\) for \(n \in \mathbb{N}\) and \(Y : \mathbb{R} \to X\) such that the pushforward of \(\lambda\) under \(Y_n\) is \(\mu_n\) for every \(n\), the pushforward of \(\lambda\) under \(Y\) is \(\mu\), and \(Y_n(t) \to Y(t)\) as \(n \to \infty\) for \(\lambda\)-almost every \(t\).

theorem skorokhod_representation
    {X : Type*} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
    (μ : ℕ → ProbabilityMeasure X) (μ₀ : ProbabilityMeasure X)
    (hμ : Filter.Tendsto (fun n => μ n) Filter.atTop (nhds μ₀)) :
    ∃ (Y : ℕ → ℝ → X) (Y₀ : ℝ → X),
      (∀ n, Measurable (Y n)) ∧ Measurable Y₀ ∧
      (∀ n, (volume.restrict (Set.Icc (0 : ℝ) (1 : ℝ))).map (Y n) = (μ n : Measure X)) ∧
      (volume.restrict (Set.Icc (0 : ℝ) (1 : ℝ))).map Y₀ = (μ₀ : Measure X) ∧
      ∀ᵐ x ∂(volume.restrict (Set.Icc (0 : ℝ) (1 : ℝ))),
        Filter.Tendsto (fun n => Y n x) Filter.atTop (nhds (Y₀ x))

Sources

• A. V. Skorokhod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290; textbook in Billingsley, Convergence of Probability Measures, 2nd ed., Foundations of Modern Probability (Icc 0 1)source,IccLebesgue base; standard version on[0, 1]` with Lebesgue.

Uses 5

Proof usesQuantile function of a real measure · The quantile function as a generalized inverse of the cdf · Monotonicity of the quantile function · Inverse transform sampling · Measurability of the quantile function

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.