def randomWalkPartialSum {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ

The n-th partial sum Sₙ(ω) = ∑_{i < n} Xᵢ(ω) of the sequence of random variables X, viewed as a random walk on ℝ.

def DriftsToTop {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → ℝ) : Prop

The random walk drifts to +∞: almost surely Sₙ → +∞ as n → ∞.

def DriftsToBot {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → ℝ) : Prop

The random walk drifts to -∞: almost surely Sₙ → -∞ as n → ∞.

def Oscillates {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → ℝ) : Prop

The random walk oscillates: almost surely limsup Sₙ = +∞ and liminf Sₙ = -∞.

def ConvergesFinite {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → ℝ) : Prop

The random walk converges to a finite limit: almost surely there exists l ∈ ℝ with Sₙ → l. In the i.i.d. dichotomy this corresponds to the degenerate case where each Xᵢ = 0.

theorem exists_prob_one_of_cover {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E₁ E₂ E₃ E₄ : Set Ω} (h_cover : μ (E₁ ∪ E₂ ∪ E₃ ∪ E₄)ᶜ = 0) (h1 : μ E₁ = 0 ∨ μ E₁ = 1) (h2 : μ E₂ = 0 ∨ μ E₂ = 1) (h3 : μ E₃ = 0 ∨ μ E₃ = 1) (h4 : μ E₄ = 0 ∨ μ E₄ = 1) : μ E₁ = 1 ∨ μ E₂ = 1 ∨ μ E₃ = 1 ∨ μ E₄ = 1

Combinatorial lemma: if four events E₁, E₂, E₃, E₄ cover the probability space modulo a null set, and each has probability either 0 or 1, then at least one of them has probability 1. This is the core dichotomy-selection step in the random-walk dichotomy proof.