Convergence in probability

TheoremConvergence in measure in the textbook ε-formulation#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), and let \(X_n : \Omega \to \mathbb{R}\) (\(n \in \mathbb{N}\)) and \(Y : \Omega \to \mathbb{R}\) be functions. Then \(X_n\) converges to \(Y\) in \(\mu\)-measure, that is, \(\mu(\{\omega : |X_n(\omega) - Y(\omega)| \ge \varepsilon\}) \to 0\) as \(n \to \infty\) for every \(\varepsilon \in (0, \infty]\), if and only if \(\mu(\{\omega : |X_n(\omega) - Y(\omega)| > \varepsilon\}) \to 0\) as \(n \to \infty\) for every real \(\varepsilon > 0\).

The second condition is the definition of convergence in probability used in the book.

theorem tendstoInMeasure_iff_tendsto_measure_abs_sub
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    {X : ℕ → Ω → ℝ} {Y : Ω → ℝ} :
    TendstoInMeasure μ X atTop Y ↔
      ∀ ε : ℝ, 0 < ε →
        Tendsto (fun n => μ {ω | ε < |X n ω - Y ω|}) atTop (𝓝 0)
Used by 1

TheoremConvergence in probability via subsequential a.s. convergence#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\Omega\), let \(X_n : \Omega \to \mathbb{R}\) (\(n \in \mathbb{N}\)) be \(\mu\)-almost everywhere strongly measurable functions, and let \(Y : \Omega \to \mathbb{R}\) be any function. Then \(\mu(\{\omega : |X_n(\omega) - Y(\omega)| > \varepsilon\}) \to 0\) as \(n \to \infty\) for every real \(\varepsilon > 0\) if and only if for every strictly increasing sequence \((n_k)\) of natural numbers there is a strictly increasing sequence \((k_j)\) of natural numbers such that \(X_{n_{k_j}}(\omega) \to Y(\omega)\) as \(j \to \infty\) for \(\mu\)-almost every \(\omega \in \Omega\).

theorem convergence_in_probability_iff_subsequential_ae_convergence
    {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
    [IsFiniteMeasure μ]
    {X : ℕ → Ω → ℝ} {Y : Ω → ℝ}
    (hX : ∀ n, AEStronglyMeasurable (X n) μ) :
    (∀ ε : ℝ, 0 < ε →
      Tendsto (fun n => μ {ω | ε < |X n ω - Y ω|}) atTop (𝓝 0)) ↔
    (∀ ns : ℕ → ℕ, StrictMono ns →
      ∃ ns' : ℕ → ℕ, StrictMono ns' ∧
        ∀ᵐ ω ∂μ, Tendsto (fun k => X (ns (ns' k)) ω) atTop (𝓝 (Y ω)))
Sources
  • Lecture 9, convergence in probability via subsequential a.s. convergence.
Uses 1
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.