theorem convergence_in_prob_iff_subseq_ae_real {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {Y : Ω → ℝ} (hX : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (X n) μ) : (∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | ε < |X n ω - Y ω|}) Filter.atTop (nhds 0)) ↔ ∀ (ns : ℕ → ℕ), StrictMono ns → ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => X (ns (ns' k)) ω) Filter.atTop (nhds (Y ω))

Convergence in probability via subsequential a.s. convergence (Lecture 9), real-valued version.

For real random variables Xₙ, Y on a finite measure space, Xₙ → Y in probability (i.e. μ{|Xₙ − Y| > ε} → 0 for every ε > 0) if and only if every subsequence of Xₙ admits a further subsequence converging to Y almost everywhere.

theorem convergence_in_probability_iff_subsequential_ae_convergence {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → ℝ} {Y : Ω → ℝ} (hX : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (X n) μ) : (∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | ε < |X n ω - Y ω|}) Filter.atTop (nhds 0)) ↔ ∀ (ns : ℕ → ℕ), StrictMono ns → ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (k : ℕ) => X (ns (ns' k)) ω) Filter.atTop (nhds (Y ω))

Theorem (convergence in probability ↔ subsequential a.s. convergence) (Lecture 9).

Xₙ → Y in probability iff for every subsequence of Xₙ there is a further subsequence converging a.s. to Y. Alias of convergence_in_prob_iff_subseq_ae_real.