@[reducible, inline]

abbrev RandomWalkTailMeasurability.sigmaAlg {Ω : Type u_1} (X : ℕ → Ω → ℝ) : ℕ → MeasurableSpace Ω

The natural filtration of σ-algebras σ(Xₙ) generated by a sequence X : ℕ → Ω → ℝ of random variables, indexed by n.

theorem RandomWalkTailMeasurability.meas_Xi {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n i : ℕ) (h : n ≤ i) : Measurable (X i)

For n ≤ i, the random variable Xᵢ is measurable with respect to the σ-algebra σ(Xₙ, Xₙ₊₁, …) (the tail σ-algebra starting from index n).

theorem RandomWalkTailMeasurability.meas_tSum {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n m : ℕ) : Measurable fun (ω : Ω) => ∑ i ∈ Finset.Ico n m, X i ω

The tail partial sum ∑_{i ∈ [n, m)} Xᵢ is measurable with respect to the σ-algebra generated by Xₙ, Xₙ₊₁, ….

theorem RandomWalkTailMeasurability.measurableSet_driftsToTop_from {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : MeasurableSet {ω : Ω | Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop Filter.atTop}

The event {Sₘ → +∞} (the partial sums of a sequence drift to +∞) lies in the tail σ-algebra starting from any index n, by expressing it as a countable Boolean combination of events measurable with respect to σ(Xₙ, Xₙ₊₁, …).

theorem RandomWalkTailMeasurability.measurableSet_driftsToBot_from {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : MeasurableSet {ω : Ω | Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop Filter.atBot}

The event {Sₘ → -∞} is measurable with respect to σ(Xₙ, Xₙ₊₁, …) for every n.

theorem RandomWalkTailMeasurability.measurableSet_limsupTop_from {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : MeasurableSet {ω : Ω | Filter.limsup (fun (m : ℕ) => ↑(randomWalkPartialSum X m ω)) Filter.atTop = ⊤}

The event {limsup Sₘ = +∞} is measurable with respect to σ(Xₙ, Xₙ₊₁, …) for every n.

theorem RandomWalkTailMeasurability.measurableSet_liminfBot_from {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : MeasurableSet {ω : Ω | Filter.liminf (fun (m : ℕ) => ↑(randomWalkPartialSum X m ω)) Filter.atTop = ⊥}

The event {liminf Sₘ = -∞} is measurable with respect to σ(Xₙ, Xₙ₊₁, …) for every n.

theorem RandomWalkTailMeasurability.measurableSet_convergesFinite_from {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) : MeasurableSet {ω : Ω | ∃ (l : ℝ), Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop (nhds l)}

The event {Sₘ converges to a finite limit} is measurable with respect to σ(Xₙ, Xₙ₊₁, …) for every n. The proof rewrites convergence as a Cauchy condition expressed via tail partial sums.

theorem RandomWalkTailMeasurability.measurableSet_driftsToTop {Ω : Type u_1} (X : ℕ → Ω → ℝ) : MeasurableSet {ω : Ω | Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop Filter.atTop}

The event {Sₘ → +∞} belongs to the tail σ-algebra of the sequence X.

theorem RandomWalkTailMeasurability.measurableSet_driftsToBot {Ω : Type u_1} (X : ℕ → Ω → ℝ) : MeasurableSet {ω : Ω | Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop Filter.atBot}

The event {Sₘ → -∞} belongs to the tail σ-algebra of the sequence X.

theorem RandomWalkTailMeasurability.measurableSet_oscillates {Ω : Type u_1} (X : ℕ → Ω → ℝ) : MeasurableSet {ω : Ω | Filter.limsup (fun (m : ℕ) => ↑(randomWalkPartialSum X m ω)) Filter.atTop = ⊤ ∧ Filter.liminf (fun (m : ℕ) => ↑(randomWalkPartialSum X m ω)) Filter.atTop = ⊥}

The oscillation event {limsup Sₘ = +∞ ∧ liminf Sₘ = -∞} belongs to the tail σ-algebra of the sequence X.

theorem RandomWalkTailMeasurability.measurableSet_convergesFinite {Ω : Type u_1} (X : ℕ → Ω → ℝ) : MeasurableSet {ω : Ω | ∃ (l : ℝ), Filter.Tendsto (fun (m : ℕ) => randomWalkPartialSum X m ω) Filter.atTop (nhds l)}

The event {Sₘ converges to a finite limit} belongs to the tail σ-algebra of the sequence X.