theorem randomWalk_events_cover_ae {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : μ ({ω : Ω | ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => randomWalkPartialSum X n ω) Filter.atTop (nhds l)} ∪ {ω : Ω | Filter.Tendsto (fun (n : ℕ) => randomWalkPartialSum X n ω) Filter.atTop Filter.atTop} ∪ {ω : Ω | Filter.Tendsto (fun (n : ℕ) => randomWalkPartialSum X n ω) Filter.atTop Filter.atBot} ∪ {ω : Ω | Filter.limsup (fun (n : ℕ) => ↑(randomWalkPartialSum X n ω)) Filter.atTop = ⊤ ∧ Filter.liminf (fun (n : ℕ) => ↑(randomWalkPartialSum X n ω)) Filter.atTop = ⊥})ᶜ = 0

Almost surely, every realization of an i.i.d. random walk falls into one of the four behavioral classes (converges to a finite limit, drifts to +∞, drifts to -∞, or oscillates between +∞ and -∞). Equivalently, the complement of the union of these four events is μ-null.

theorem random_walk_dichotomy {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : ConvergesFinite μ X ∨ DriftsToTop μ X ∨ DriftsToBot μ X ∨ Oscillates μ X

Random walk dichotomy (Durrett, Lecture 23). If X₁, X₂, … are i.i.d. real-valued random variables and Sₙ = ∑_{i<n} Xᵢ, then with probability one exactly one of the following occurs:

• Sₙ → l for some finite l (degenerate case Xᵢ ≡ 0),
• Sₙ → +∞,
• Sₙ → -∞,
• liminf Sₙ = -∞ and limsup Sₙ = +∞ (the walk oscillates).