Drift and oscillation of random walks

Definitionσ-algebra generated by a tail of a sequence of σ-algebras#✓fully proved

Given σ-algebras \(\mathcal{A}_0, \mathcal{A}_1, \dots\) on \(\Omega\) and \(n \in \mathbb{N}\), this is \(\sigma(\mathcal{A}_n, \mathcal{A}_{n+1}, \dots)\), the smallest σ-algebra on \(\Omega\) containing every \(\mathcal{A}_i\) with \(i \ge n\).

@[reducible]
def tailMeasurableSpaceFrom (𝓐 : ℕ → MeasurableSpace Ω) (n : ℕ) : MeasurableSpace Ω :=
  ⨆ (i : ℕ) (_ : n ≤ i), 𝓐 i
Used by 12
Used byTail partial sums are measurable for the σ-algebra from their first index · Later terms are measurable for the σ-algebra from a given index · Convergence of a random walk is a tail event · Convergence of a random walk is measurable from every index · Drift of a random walk to −∞ is a tail event · Drift of a random walk to −∞ is measurable from every index · Drift of a random walk to +∞ is a tail event · Drift of a random walk to +∞ is measurable from every index · A limit inferior −∞ of a random walk is measurable from every index · A limit superior +∞ of a random walk is measurable from every index · Tail measurability of the oscillation event · Tail σ-algebra of a sequence of σ-algebras

DefinitionTail σ-algebra of a sequence of σ-algebras#✓fully proved

Given σ-algebras \(\mathcal{A}_0, \mathcal{A}_1, \dots\) on \(\Omega\), the tail σ-algebra is

\[\mathcal{T} = \bigcap_{n \in \mathbb{N}} \sigma(\mathcal{A}_n, \mathcal{A}_{n+1}, \dots),\]

where \(\sigma(\mathcal{A}_n, \mathcal{A}_{n+1}, \dots)\) is the smallest σ-algebra containing every \(\mathcal{A}_i\) with \(i \ge n\). It contains the information observable by looking only at events arbitrarily far into the future.

@[reducible]
def tailMeasurableSpace (𝓐 : ℕ → MeasurableSpace Ω) : MeasurableSpace Ω :=
  ⨅ n, tailMeasurableSpaceFrom 𝓐 n
Uses 1 · Used by 1
Statement usesσ-algebra generated by a tail of a sequence of σ-algebras
Used byTail σ-algebra of a sequence of functions

AbbreviationTail σ-algebra of a sequence of functions#✓fully proved

Let \(\beta\) be a measurable space and let \(X_n : \Omega \to \beta\) for \(n \in \mathbb{N}\). The tail σ-algebra of \(X\) is

\[\mathcal{T} = \bigcap_{n \in \mathbb{N}} \sigma(X_n, X_{n+1}, \dots),\]

the tail σ-algebra of the sequence of σ-algebras \(\sigma(X_n)\), where \(\sigma(X_n)\) consists of the preimages under \(X_n\) of measurable subsets of \(\beta\). This is the tail σ-algebra appearing in Kolmogorov's 0-1 law.

abbrev tailMeasurableSpaceOfFun {β : Type*} [MeasurableSpace β] (X : ℕ → Ω → β) :
    MeasurableSpace Ω :=
  tailMeasurableSpace (fun n => MeasurableSpace.comap (X n) ‹_›)
Uses 1 · Used by 4
Statement usesTail σ-algebra of a sequence of σ-algebras
Used byConvergence of a random walk is a tail event · Drift of a random walk to −∞ is a tail event · Drift of a random walk to +∞ is a tail event · Tail measurability of the oscillation event

DefinitionPartial sums of a random walk#✓fully proved

For a sequence of functions \(X_i : \Omega \to \mathbb{R}\) and \(n \in \mathbb{N}\), the \(n\)-th partial sum is \(S_n(\omega) = \sum_{i < n} X_i(\omega)\), the position at time \(n\) of the random walk on \(\mathbb{R}\) with increments \(X_i\).

def randomWalkPartialSum (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  ∑ i ∈ Finset.range n, X i ω
Used by 28
Used byRandom walk with a finite limit · Vanishing steps give a convergent random walk · Random-walk dichotomy on sequence space · Random walk drifting to \(-\infty\) · Random walk drifting to \(+\infty\) · Finite permutations do not change the liminf of the partial sums · One-step shift identity for the liminf of the partial sums · Finite permutations do not change the limsup of the partial sums · One-step shift identity for the limsup of partial sums · Convergence of a random walk is a tail event · Convergence of a random walk is measurable from every index · The convergence event on sequence space is measurable · The event of drift to \(-\infty\) on sequence space is measurable · The event of drift to \(+\infty\) on sequence space is measurable · The oscillation event on sequence space is measurable · Drift of a random walk to −∞ is a tail event · Drift of a random walk to −∞ is measurable from every index · Drift of a random walk to +∞ is a tail event · Drift of a random walk to +∞ is measurable from every index · A limit inferior −∞ of a random walk is measurable from every index · A limit superior +∞ of a random walk is measurable from every index · Tail measurability of the oscillation event · Partial sums are unchanged by permuting the first coordinates · Random-walk dichotomy · Liminf of a random walk · Limsup of a random walk · Zero random walk · A random walk is zero exactly when its steps are

Abbreviationσ-algebras generated by a sequence of functions#✓fully proved

For a sequence of functions \(X_n : \Omega \to \mathbb{R}\), this is the sequence of σ-algebras \(\sigma(X_n)\) on \(\Omega\), where \(\sigma(X_n)\) consists of the preimages under \(X_n\) of Borel subsets of \(\mathbb{R}\).

abbrev sigmaAlg (X : ℕ → Ω → ℝ) : ℕ → MeasurableSpace Ω :=
  fun n => MeasurableSpace.comap (X n) inferInstance
Used by 8
Used byTail partial sums are measurable for the σ-algebra from their first index · Later terms are measurable for the σ-algebra from a given index · Convergence of a random walk is measurable from every index · Drift of a random walk to −∞ is measurable from every index · Drift of a random walk to +∞ is measurable from every index · A limit inferior −∞ of a random walk is measurable from every index · A limit superior +∞ of a random walk is measurable from every index · Tail measurability of the oscillation event

LemmaLater terms are measurable for the σ-algebra from a given index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. If \(n \le i\), then \(X_i\) is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

lemma meas_Xi (X : ℕ → Ω → ℝ) (n i : ℕ) (h : n ≤ i) :
    @Measurable _ _ (tailMeasurableSpaceFrom (sigmaAlg X) n) _ (X i)
Uses 2 · Used by 1
Statement usesσ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Used byTail partial sums are measurable for the σ-algebra from their first index

LemmaTail partial sums are measurable for the σ-algebra from their first index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For all \(n, m \in \mathbb{N}\), the function \(\omega \mapsto \sum_{n \le i < m} X_i(\omega)\) is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

lemma meas_tSum (X : ℕ → Ω → ℝ) (n m : ℕ) :
    @Measurable _ _ (tailMeasurableSpaceFrom (sigmaAlg X) n) _
      (fun ω => ∑ i ∈ Ico n m, X i ω)
Uses 3 · Used by 5
Statement usesσ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesLater terms are measurable for the σ-algebra from a given index
Used byConvergence of a random walk is measurable from every index · Drift of a random walk to −∞ is measurable from every index · Drift of a random walk to +∞ is measurable from every index · A limit inferior −∞ of a random walk is measurable from every index · A limit superior +∞ of a random walk is measurable from every index

TheoremDrift of a random walk to +∞ is measurable from every index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), let \(S_m = \sum_{i < m} X_i\) be their partial sums, and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For every \(n\), the set of \(\omega \in \Omega\) with \(S_m(\omega) \to +\infty\) as \(m \to \infty\) is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

The proof writes this set as a countable Boolean combination of sets defined by the tail partial sums \(\sum_{n \le i < m} X_i\).

theorem measurableSet_driftsToTop_from (X : ℕ → Ω → ℝ) (n : ℕ) :
    @MeasurableSet _ (tailMeasurableSpaceFrom (sigmaAlg X) n)
      {ω | Tendsto (fun m => randomWalkPartialSum X m ω) atTop atTop}
Uses 4 · Used by 1
Statement usesPartial sums of a random walk · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesTail partial sums are measurable for the σ-algebra from their first index
Used byDrift of a random walk to +∞ is a tail event

TheoremDrift of a random walk to −∞ is measurable from every index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), let \(S_m = \sum_{i < m} X_i\) be their partial sums, and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For every \(n\), the set of \(\omega \in \Omega\) with \(S_m(\omega) \to -\infty\) as \(m \to \infty\) is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

theorem measurableSet_driftsToBot_from (X : ℕ → Ω → ℝ) (n : ℕ) :
    @MeasurableSet _ (tailMeasurableSpaceFrom (sigmaAlg X) n)
      {ω | Tendsto (fun m => randomWalkPartialSum X m ω) atTop atBot}
Uses 4 · Used by 1
Statement usesPartial sums of a random walk · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesTail partial sums are measurable for the σ-algebra from their first index
Used byDrift of a random walk to −∞ is a tail event

TheoremA limit superior +∞ of a random walk is measurable from every index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), let \(S_m = \sum_{i < m} X_i\) be their partial sums, and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For every \(n\), the set of \(\omega \in \Omega\) with \(\limsup_{m \to \infty} S_m(\omega) = +\infty\), the limit superior taken in the extended reals, is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

theorem measurableSet_limsupTop_from (X : ℕ → Ω → ℝ) (n : ℕ) :
    @MeasurableSet _ (tailMeasurableSpaceFrom (sigmaAlg X) n)
      {ω | limsup (fun m => ((randomWalkPartialSum X m ω : ℝ) : EReal)) atTop = ⊤}
Uses 4 · Used by 1
Statement usesPartial sums of a random walk · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesTail partial sums are measurable for the σ-algebra from their first index
Used byTail measurability of the oscillation event

TheoremA limit inferior −∞ of a random walk is measurable from every index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), let \(S_m = \sum_{i < m} X_i\) be their partial sums, and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For every \(n\), the set of \(\omega \in \Omega\) with \(\liminf_{m \to \infty} S_m(\omega) = -\infty\), the limit inferior taken in the extended reals, is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

theorem measurableSet_liminfBot_from (X : ℕ → Ω → ℝ) (n : ℕ) :
    @MeasurableSet _ (tailMeasurableSpaceFrom (sigmaAlg X) n)
      {ω | liminf (fun m => ((randomWalkPartialSum X m ω : ℝ) : EReal)) atTop = ⊥}
Uses 4 · Used by 1
Statement usesPartial sums of a random walk · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesTail partial sums are measurable for the σ-algebra from their first index
Used byTail measurability of the oscillation event

TheoremConvergence of a random walk is measurable from every index#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\), let \(S_m = \sum_{i < m} X_i\) be their partial sums, and for \(n \in \mathbb{N}\) let \(\sigma(X_n, X_{n+1}, \dots)\) be the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable. For every \(n\), the set of \(\omega \in \Omega\) for which \(S_m(\omega)\) converges to a real limit as \(m \to \infty\) is measurable with respect to \(\sigma(X_n, X_{n+1}, \dots)\).

The proof rewrites convergence as a Cauchy condition on the tail partial sums \(\sum_{n \le i < m} X_i\).

theorem measurableSet_convergesFinite_from (X : ℕ → Ω → ℝ) (n : ℕ) :
    @MeasurableSet _ (tailMeasurableSpaceFrom (sigmaAlg X) n)
      {ω | ∃ l : ℝ, Tendsto (fun m => randomWalkPartialSum X m ω) atTop (𝓝 l)}
Uses 4 · Used by 1
Statement usesPartial sums of a random walk · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras
Proof usesTail partial sums are measurable for the σ-algebra from their first index
Used byConvergence of a random walk is a tail event

TheoremDrift of a random walk to +∞ is a tail event#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\) and let \(S_m = \sum_{i < m} X_i\) be their partial sums. The set of \(\omega \in \Omega\) with \(S_m(\omega) \to +\infty\) as \(m \to \infty\) belongs to the tail σ-algebra \(\bigcap_{n} \sigma(X_n, X_{n+1}, \dots)\) of the sequence, where \(\sigma(X_n, X_{n+1}, \dots)\) is the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable.

theorem measurableSet_driftsToTop (X : ℕ → Ω → ℝ) :
    @MeasurableSet _ (tailMeasurableSpaceOfFun X)
      {ω | Tendsto (fun m => randomWalkPartialSum X m ω) atTop atTop}
Uses 4
Statement usesPartial sums of a random walk · Tail σ-algebra of a sequence of functions
Proof usesDrift of a random walk to +∞ is measurable from every index · σ-algebra generated by a tail of a sequence of σ-algebras

TheoremDrift of a random walk to −∞ is a tail event#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\) and let \(S_m = \sum_{i < m} X_i\) be their partial sums. The set of \(\omega \in \Omega\) with \(S_m(\omega) \to -\infty\) as \(m \to \infty\) belongs to the tail σ-algebra \(\bigcap_{n} \sigma(X_n, X_{n+1}, \dots)\) of the sequence, where \(\sigma(X_n, X_{n+1}, \dots)\) is the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable.

theorem measurableSet_driftsToBot (X : ℕ → Ω → ℝ) :
    @MeasurableSet _ (tailMeasurableSpaceOfFun X)
      {ω | Tendsto (fun m => randomWalkPartialSum X m ω) atTop atBot}
Uses 4
Statement usesPartial sums of a random walk · Tail σ-algebra of a sequence of functions
Proof usesDrift of a random walk to −∞ is measurable from every index · σ-algebra generated by a tail of a sequence of σ-algebras

TheoremTail measurability of the oscillation event#✓fully proved

Let \(X_n : \Omega \to \mathbb{R}\) for \(n \in \mathbb{N}\) be a sequence of functions with partial sums \(S_m = \sum_{i < m} X_i\). Then the event that \(\limsup_{m \to \infty} S_m = +\infty\) and \(\liminf_{m \to \infty} S_m = -\infty\), with the limit superior and inferior taken in the extended reals, belongs to the tail σ-algebra of \(X\).

theorem measurableSet_oscillates (X : ℕ → Ω → ℝ) :
    @MeasurableSet _ (tailMeasurableSpaceOfFun X)
      {ω | limsup (fun m => ((randomWalkPartialSum X m ω : ℝ) : EReal)) atTop = ⊤ ∧
           liminf (fun m => ((randomWalkPartialSum X m ω : ℝ) : EReal)) atTop = ⊥}
Uses 6
Statement usesPartial sums of a random walk · Tail σ-algebra of a sequence of functions
Proof usesA limit inferior −∞ of a random walk is measurable from every index · A limit superior +∞ of a random walk is measurable from every index · σ-algebras generated by a sequence of functions · σ-algebra generated by a tail of a sequence of σ-algebras

TheoremConvergence of a random walk is a tail event#✓fully proved

Let \(X_0, X_1, \dots\) be real-valued functions on a set \(\Omega\) and let \(S_m = \sum_{i < m} X_i\) be their partial sums. The set of \(\omega \in \Omega\) for which \(S_m(\omega)\) converges to a real limit as \(m \to \infty\) belongs to the tail σ-algebra \(\bigcap_{n} \sigma(X_n, X_{n+1}, \dots)\) of the sequence, where \(\sigma(X_n, X_{n+1}, \dots)\) is the smallest σ-algebra on \(\Omega\) for which every \(X_i\) with \(i \ge n\) is Borel measurable.

theorem measurableSet_convergesFinite (X : ℕ → Ω → ℝ) :
    @MeasurableSet _ (tailMeasurableSpaceOfFun X)
      {ω | ∃ l : ℝ, Tendsto (fun m => randomWalkPartialSum X m ω) atTop (𝓝 l)}
Uses 4
Statement usesPartial sums of a random walk · Tail σ-algebra of a sequence of functions
Proof usesConvergence of a random walk is measurable from every index · σ-algebra generated by a tail of a sequence of σ-algebras

DefinitionLimsup of a random walk#✓fully proved

For real-valued functions \(X_0, X_1, \dots\) on a set \(\Omega\) and a point \(\omega \in \Omega\), this is \(\limsup_{n \to \infty} S_n(\omega)\), taken in the extended reals \([-\infty, +\infty]\), where \(S_n(\omega) = \sum_{i < n} X_i(\omega)\) is the \(n\)-th partial sum.

noncomputable def randomWalkLimsup {Ω : Type*} (X : ℕ → Ω → ℝ) (ω : Ω) : EReal :=
  Filter.limsup (fun n => ((randomWalkPartialSum X n ω : ℝ) : EReal)) Filter.atTop
Uses 1 · Used by 6
Statement usesPartial sums of a random walk
Used byRandom-walk dichotomy on sequence space · Finite permutations do not change the limsup of the partial sums · One-step shift identity for the limsup of partial sums · The oscillation event on sequence space is measurable · Oscillating random walk · Random-walk dichotomy

DefinitionLiminf of a random walk#✓fully proved

For real-valued functions \(X_0, X_1, \dots\) on a set \(\Omega\) and a point \(\omega \in \Omega\), this is \(\liminf_{n \to \infty} S_n(\omega)\), taken in the extended reals \([-\infty, +\infty]\), where \(S_n(\omega) = \sum_{i < n} X_i(\omega)\) is the \(n\)-th partial sum.

noncomputable def randomWalkLiminf {Ω : Type*} (X : ℕ → Ω → ℝ) (ω : Ω) : EReal :=
  Filter.liminf (fun n => ((randomWalkPartialSum X n ω : ℝ) : EReal)) Filter.atTop
Uses 1 · Used by 6
Statement usesPartial sums of a random walk
Used byRandom-walk dichotomy on sequence space · Finite permutations do not change the liminf of the partial sums · One-step shift identity for the liminf of the partial sums · The oscillation event on sequence space is measurable · Oscillating random walk · Random-walk dichotomy

DefinitionShift of a real sequence#✓fully proved

The one-step shift sends a real sequence \(\omega = (\omega_0, \omega_1, \omega_2, \dots)\) to the sequence \((\omega_1, \omega_2, \dots)\) whose \(i\)-th term is \(\omega_{i+1}\).

def shiftSeq (ω : ℕ → ℝ) : ℕ → ℝ := fun i => ω (i + 1)
Used by 4
Used byRandom-walk dichotomy on sequence space · One-step shift identity for the liminf of the partial sums · One-step shift identity for the limsup of partial sums · Shift invariance of the i.i.d. product measure

DefinitionCoordinate process on sequence space#✓fully proved

For \(i \in \mathbb{N}\), the \(i\)-th coordinate is the map \(\mathbb{R}^{\mathbb{N}} \to \mathbb{R}\) sending a real sequence \(\omega = (\omega_0, \omega_1, \dots)\) to its \(i\)-th term \(\omega_i\).

def coordSeq (i : ℕ) (ω : ℕ → ℝ) : ℝ := ω i
Used by 12
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy on sequence space · Finite permutations do not change the liminf of the partial sums · One-step shift identity for the liminf of the partial sums · Finite permutations do not change the limsup of the partial sums · One-step shift identity for the limsup of partial sums · The convergence event on sequence space is measurable · The event of drift to \(-\infty\) on sequence space is measurable · The event of drift to \(+\infty\) on sequence space is measurable · The oscillation event on sequence space is measurable · Partial sums are unchanged by permuting the first coordinates · Random-walk dichotomy

TheoremDropping the first term preserves the limsup#✓fully proved

For every sequence \((u_n)_{n \in \mathbb{N}}\) of extended reals, \(\limsup_{n \to \infty} u_{n+1} = \limsup_{n \to \infty} u_n\).

theorem limsup_succ_eq {u : ℕ → EReal} :
    Filter.limsup (fun n => u (n + 1)) Filter.atTop = Filter.limsup u Filter.atTop
Used by 1
Used byOne-step shift identity for the limsup of partial sums

TheoremDropping the first term does not change the liminf#✓fully proved

For every sequence \((u_n)\) in the extended reals \([-\infty, +\infty]\), \(\liminf_{n \to \infty} u_{n+1} = \liminf_{n \to \infty} u_n\).

theorem liminf_succ_eq {u : ℕ → EReal} :
    Filter.liminf (fun n => u (n + 1)) Filter.atTop = Filter.liminf u Filter.atTop
Used by 1
Used byOne-step shift identity for the liminf of the partial sums

TheoremLimsup commutes with adding a constant#✓fully proved

For every real \(c\) and every real sequence \((u_n)\), with limits superior taken in the extended reals \([-\infty, +\infty]\), \(\limsup_{n \to \infty} (c + u_n) = c + \limsup_{n \to \infty} u_n\).

theorem limsup_add_const (c : ℝ) (u : ℕ → ℝ) :
    Filter.limsup (fun n => ((c + u n : ℝ) : EReal)) Filter.atTop =
      (c : EReal) + Filter.limsup (fun n => ((u n : ℝ) : EReal)) Filter.atTop
Used by 1
Used byOne-step shift identity for the limsup of partial sums

TheoremLiminf commutes with adding a constant#✓fully proved

For every real \(c\) and every real sequence \((u_n)\), with limits inferior taken in the extended reals \([-\infty, +\infty]\), \(\liminf_{n \to \infty} (c + u_n) = c + \liminf_{n \to \infty} u_n\).

theorem liminf_add_const (c : ℝ) (u : ℕ → ℝ) :
    Filter.liminf (fun n => ((c + u n : ℝ) : EReal)) Filter.atTop =
      (c : EReal) + Filter.liminf (fun n => ((u n : ℝ) : EReal)) Filter.atTop
Used by 1
Used byOne-step shift identity for the liminf of the partial sums

TheoremOne-step shift identity for the limsup of partial sums#✓fully proved

For a real sequence \(\omega = (\omega_0, \omega_1, \dots)\) write \(S_n(\omega) = \sum_{i < n} \omega_i\), and let \(\theta\omega = (\omega_1, \omega_2, \dots)\) be the one-step shift. Then for every \(\omega\), \(\limsup_{n \to \infty} S_n(\omega) = \omega_0 + \limsup_{n \to \infty} S_n(\theta\omega)\), where both limits superior are taken in the extended reals \([-\infty, +\infty]\).

theorem limsup_shift (ω : ℕ → ℝ) :
    randomWalkLimsup coordSeq ω =
      (ω 0 : EReal) + randomWalkLimsup coordSeq (shiftSeq ω)
Uses 6 · Used by 1
Statement usesCoordinate process on sequence space · Limsup of a random walk · Shift of a real sequence
Proof usesLimsup commutes with adding a constant · Dropping the first term preserves the limsup · Partial sums of a random walk
Used byRandom-walk dichotomy on sequence space

TheoremOne-step shift identity for the liminf of the partial sums#✓fully proved

For a real sequence \(\omega = (\omega_0, \omega_1, \dots)\) write \(S_n(\omega) = \sum_{i\lt n} \omega_i\), and let \(\omega'\) be its shift, \(\omega'_i = \omega_{i+1}\). Then, with limits inferior taken in \([-\infty, +\infty]\), we have \(\liminf_{n \to \infty} S_n(\omega) = \omega_0 + \liminf_{n \to \infty} S_n(\omega')\).

theorem liminf_shift (ω : ℕ → ℝ) :
    randomWalkLiminf coordSeq ω =
      (ω 0 : EReal) + randomWalkLiminf coordSeq (shiftSeq ω)
Uses 6 · Used by 1
Statement usesCoordinate process on sequence space · Liminf of a random walk · Shift of a real sequence
Proof usesLiminf commutes with adding a constant · Dropping the first term does not change the liminf · Partial sums of a random walk
Used byRandom-walk dichotomy on sequence space

TheoremPartial sums are unchanged by permuting the first coordinates#✓fully proved

Let \(\sigma\) be a permutation of \(\mathbb{N}\) with \(\sigma(m) = m\) for every \(m \ge N\). Then for every real sequence \((\omega_i)_{i \in \mathbb{N}}\) and every \(n \ge N\), \(\sum_{i < n} \omega_{\sigma(i)} = \sum_{i < n} \omega_i\).

theorem partialSum_comp_perm_eq {σ : Equiv.Perm ℕ} {N : ℕ}
    (hσ : ∀ m, m ≥ N → σ m = m) {ω : ℕ → ℝ} {n : ℕ} (hn : n ≥ N) :
    randomWalkPartialSum coordSeq n (ω ∘ ⇑σ) =
      randomWalkPartialSum coordSeq n ω
Uses 2 · Used by 2
Statement usesCoordinate process on sequence space · Partial sums of a random walk
Used byFinite permutations do not change the liminf of the partial sums · Finite permutations do not change the limsup of the partial sums

TheoremFinite permutations do not change the limsup of the partial sums#✓fully proved

Let \(\sigma\) be a permutation of \(\mathbb{N}\) that moves only finitely many points. For every real sequence \(\omega = (\omega_0, \omega_1, \dots)\), the limit superior in \([-\infty, +\infty]\) of the partial sums \(\sum_{i\lt n} \omega_{\sigma(i)}\) equals the limit superior of the partial sums \(\sum_{i\lt n} \omega_i\).

theorem limsup_comp_perm {σ : Equiv.Perm ℕ} (hσ : Set.Finite {n : ℕ | σ n ≠ n})
    (ω : ℕ → ℝ) :
    randomWalkLimsup coordSeq (ω ∘ ⇑σ) = randomWalkLimsup coordSeq ω
Uses 4 · Used by 1
Statement usesCoordinate process on sequence space · Limsup of a random walk
Proof usesPartial sums are unchanged by permuting the first coordinates · Partial sums of a random walk
Used byRandom-walk dichotomy on sequence space

TheoremFinite permutations do not change the liminf of the partial sums#✓fully proved

Let \(\sigma\) be a permutation of \(\mathbb{N}\) that moves only finitely many points. For every real sequence \(\omega = (\omega_0, \omega_1, \dots)\), the limit inferior in \([-\infty, +\infty]\) of the partial sums \(\sum_{i\lt n} \omega_{\sigma(i)}\) equals the limit inferior of the partial sums \(\sum_{i\lt n} \omega_i\).

theorem liminf_comp_perm {σ : Equiv.Perm ℕ} (hσ : Set.Finite {n : ℕ | σ n ≠ n})
    (ω : ℕ → ℝ) :
    randomWalkLiminf coordSeq (ω ∘ ⇑σ) = randomWalkLiminf coordSeq ω
Uses 4 · Used by 1
Statement usesCoordinate process on sequence space · Liminf of a random walk
Proof usesPartial sums are unchanged by permuting the first coordinates · Partial sums of a random walk
Used byRandom-walk dichotomy on sequence space

TheoremShift invariance of the i.i.d. product measure#✓fully proved

Let \(\rho\) be a probability measure on \(\mathbb{R}\), and let \(\rho^{\otimes \mathbb{N}}\) be the product measure on the sequence space \(\mathbb{R}^{\mathbb{N}}\). The image of \(\rho^{\otimes \mathbb{N}}\) under the one-step shift \((\omega_0, \omega_1, \dots) \mapsto (\omega_1, \omega_2, \dots)\) is \(\rho^{\otimes \mathbb{N}}\).

theorem map_shiftSeq_infinitePi (ρ : Measure ℝ) [IsProbabilityMeasure ρ] :
    (Measure.infinitePi (fun _ : ℕ => ρ)).map shiftSeq =
      Measure.infinitePi (fun _ : ℕ => ρ)
Uses 1 · Used by 1
Statement usesShift of a real sequence
Used byRandom-walk dichotomy on sequence space

TheoremZero–one sublevel sets force an almost surely constant variable#✓fully proved

Let \(\mu\) be a probability measure on \(\Omega\) and let \(F : \Omega \to [-\infty, +\infty]\) be measurable. If for every real \(a\) the set \(\{\omega : F(\omega) \le a\}\) has \(\mu\)-measure \(0\) or \(1\), then there is \(c \in [-\infty, +\infty]\) with \(F = c\) \(\mu\)-almost everywhere.

theorem exists_ae_eq_const_of_forall_le_zero_or_one {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {F : Ω → EReal}
    (hF : Measurable F)
    (h01 : ∀ a : ℝ, μ {ω | F ω ≤ (a : EReal)} = 0 ∨ μ {ω | F ω ≤ (a : EReal)} = 1) :
    ∃ c : EReal, ∀ᵐ ω ∂μ, F ω = c
Used by 1
Used byRandom-walk dichotomy on sequence space

TheoremLimsup minus infinity forces divergence to minus infinity#✓fully proved

Let \((S_n)\) be a sequence of real numbers. If \(\limsup_{n \to \infty} S_n = -\infty\) in the extended reals, then \(S_n \to -\infty\) as \(n \to \infty\).

theorem tendsto_atBot_of_limsup_eq_bot {S : ℕ → ℝ}
    (h : Filter.limsup (fun n => ((S n : ℝ) : EReal)) Filter.atTop = ⊥) :
    Tendsto S Filter.atTop Filter.atBot
Used by 1
Used byRandom-walk dichotomy on sequence space

TheoremA sequence tending to \(-\infty\) has limsup \(-\infty\)#✓fully proved

Let \((S_n)_{n \in \mathbb{N}}\) be a sequence of real numbers with \(S_n \to -\infty\) as \(n \to \infty\). Then the limit superior of \((S_n)\), taken in the extended reals \([-\infty, +\infty]\), equals \(-\infty\).

theorem limsup_eq_bot_of_tendsto_atBot {S : ℕ → ℝ}
    (h : Tendsto S Filter.atTop Filter.atBot) :
    Filter.limsup (fun n => ((S n : ℝ) : EReal)) Filter.atTop = ⊥

TheoremLiminf plus infinity forces divergence to plus infinity#✓fully proved

Let \((S_n)\) be a sequence of real numbers. If \(\liminf_{n \to \infty} S_n = +\infty\) in the extended reals, then \(S_n \to +\infty\) as \(n \to \infty\).

theorem tendsto_atTop_of_liminf_eq_top {S : ℕ → ℝ}
    (h : Filter.liminf (fun n => ((S n : ℝ) : EReal)) Filter.atTop = ⊤) :
    Tendsto S Filter.atTop Filter.atTop
Used by 1
Used byRandom-walk dichotomy on sequence space

TheoremA real sequence tending to \(+\infty\) has liminf \(+\infty\)#✓fully proved

If a real sequence \((S_n)\) tends to \(+\infty\), then its limit inferior in the extended reals \([-\infty, +\infty]\) is \(+\infty\).

theorem liminf_eq_top_of_tendsto_atTop {S : ℕ → ℝ}
    (h : Tendsto S Filter.atTop Filter.atTop) :
    Filter.liminf (fun n => ((S n : ℝ) : EReal)) Filter.atTop = ⊤

TheoremThe event of drift to \(+\infty\) on sequence space is measurable#✓fully proved

Equip \(\mathbb{R}^{\mathbb{N}}\) with its product σ-algebra and write \(S_n(\omega) = \sum_{i < n} \omega_i\). The set of \(\omega \in \mathbb{R}^{\mathbb{N}}\) with \(S_n(\omega) \to +\infty\) as \(n \to \infty\) is measurable.

theorem measurableSet_coord_driftsToTop :
    MeasurableSet {ω : ℕ → ℝ |
      Tendsto (fun n => randomWalkPartialSum coordSeq n ω) Filter.atTop Filter.atTop}
Uses 2 · Used by 1
Statement usesCoordinate process on sequence space · Partial sums of a random walk
Used byRandom-walk dichotomy

TheoremThe event of drift to \(-\infty\) on sequence space is measurable#✓fully proved

Equip \(\mathbb{R}^{\mathbb{N}}\) with its product σ-algebra and write \(S_n(\omega) = \sum_{i < n} \omega_i\). The set of \(\omega \in \mathbb{R}^{\mathbb{N}}\) with \(S_n(\omega) \to -\infty\) as \(n \to \infty\) is measurable.

theorem measurableSet_coord_driftsToBot :
    MeasurableSet {ω : ℕ → ℝ |
      Tendsto (fun n => randomWalkPartialSum coordSeq n ω) Filter.atTop Filter.atBot}
Uses 2 · Used by 1
Statement usesCoordinate process on sequence space · Partial sums of a random walk
Used byRandom-walk dichotomy

TheoremThe oscillation event on sequence space is measurable#✓fully proved

Equip \(\mathbb{R}^{\mathbb{N}}\) with its product σ-algebra and write \(S_n(\omega) = \sum_{i < n} \omega_i\). The set of \(\omega \in \mathbb{R}^{\mathbb{N}}\) with \(\limsup_{n \to \infty} S_n(\omega) = +\infty\) and \(\liminf_{n \to \infty} S_n(\omega) = -\infty\) (limits taken in the extended reals) is measurable.

theorem measurableSet_coord_oscillates :
    MeasurableSet {ω : ℕ → ℝ |
      randomWalkLimsup coordSeq ω = ⊤ ∧ randomWalkLiminf coordSeq ω = ⊥}
Uses 4
Statement usesCoordinate process on sequence space · Liminf of a random walk · Limsup of a random walk
Proof usesPartial sums of a random walk

TheoremThe zero-sequence event is measurable#✓fully proved

In the sequence space \(\mathbb{R}^{\mathbb{N}}\) with its product σ-algebra, the set of sequences \(\omega\) with \(\omega_i = 0\) for every \(i\) is measurable.

theorem measurableSet_coord_forall_eq_zero :
    MeasurableSet {ω : ℕ → ℝ | ∀ i, ω i = 0}
Used by 1
Used byRandom-walk dichotomy

TheoremVanishing steps give a convergent random walk#✓fully proved

Let \(\mu\) be a measure on \(\Omega\) and let \(X_0, X_1, \dots\) be real-valued functions on \(\Omega\), with partial sums \(S_n = \sum_{i\lt n} X_i\). If for \(\mu\)-almost every \(\omega\) we have \(X_i(\omega) = 0\) for all \(i\), then for \(\mu\)-almost every \(\omega\) the sequence \(S_n(\omega)\) converges to a finite real limit.

theorem convergesFinite_of_ae_forall_eq_zero {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {X : ℕ → Ω → ℝ} (h : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0) :
    ∀ᵐ ω ∂μ, ∃ l : ℝ, Tendsto (fun n => randomWalkPartialSum X n ω) Filter.atTop
      (𝓝 l)
Uses 1 · Used by 1
Statement usesPartial sums of a random walk
Used byA zero walk converges to a finite limit

TheoremThe convergence event on sequence space is measurable#✓fully proved

Equip \(\mathbb{R}^{\mathbb{N}}\) with its product σ-algebra and write \(S_n(\omega) = \sum_{i < n} \omega_i\). The set of \(\omega \in \mathbb{R}^{\mathbb{N}}\) for which \(S_n(\omega)\) converges to a finite real limit as \(n \to \infty\) is measurable.

theorem measurableSet_coord_convergesFinite :
    MeasurableSet {ω : ℕ → ℝ | ∃ l : ℝ,
      Tendsto (fun n => randomWalkPartialSum coordSeq n ω) Filter.atTop (𝓝 l)}
Uses 2
Statement usesCoordinate process on sequence space · Partial sums of a random walk

DefinitionZero random walk#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \ldots\) be real-valued functions on \(\Omega\), and let \(S_n = \sum_{i < n} X_i\) be the partial sums of the random walk. The walk is a zero walk when, for \(\mu\)-almost every \(\omega \in \Omega\), we have \(S_n(\omega) = 0\) for every \(n \in \mathbb{N}\).

def ZeroWalk {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) : Prop :=
  ∀ᵐ ω ∂μ, ∀ n, randomWalkPartialSum X n ω = 0
Uses 1 · Used by 6
Statement usesPartial sums of a random walk
Used byA zero walk converges to a finite limit · Random-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy on sequence space · Random-walk dichotomy, finite-limit form · Random-walk dichotomy · A random walk is zero exactly when its steps are

DefinitionRandom walk drifting to \(+\infty\)#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space \((\Omega, \mu)\) and \(S_n = \sum_{i < n} X_i\). The random walk \((S_n)\) drifts to \(+\infty\) if for \(\mu\)-almost every \(\omega\), \(S_n(\omega) \to +\infty\) as \(n \to \infty\).

def DriftsToTop {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) : Prop :=
  ∀ᵐ ω ∂μ, Tendsto (fun n => randomWalkPartialSum X n ω) Filter.atTop Filter.atTop
Uses 1 · Used by 4
Statement usesPartial sums of a random walk
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy on sequence space · Random-walk dichotomy, finite-limit form · Random-walk dichotomy

DefinitionRandom walk drifting to \(-\infty\)#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space \((\Omega, \mu)\) and \(S_n = \sum_{i < n} X_i\). The random walk \((S_n)\) drifts to \(-\infty\) if for \(\mu\)-almost every \(\omega\), \(S_n(\omega) \to -\infty\) as \(n \to \infty\).

def DriftsToBot {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) : Prop :=
  ∀ᵐ ω ∂μ, Tendsto (fun n => randomWalkPartialSum X n ω) Filter.atTop Filter.atBot
Uses 1 · Used by 4
Statement usesPartial sums of a random walk
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy on sequence space · Random-walk dichotomy, finite-limit form · Random-walk dichotomy

DefinitionOscillating random walk#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space \((\Omega, \mu)\) and \(S_n = \sum_{i < n} X_i\). The random walk \((S_n)\) oscillates if for \(\mu\)-almost every \(\omega\), \(\limsup_n S_n(\omega) = +\infty\) and \(\liminf_n S_n(\omega) = -\infty\), the limits taken in the extended reals.

def Oscillates {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) : Prop :=
  ∀ᵐ ω ∂μ, randomWalkLimsup X ω = ⊤ ∧ randomWalkLiminf X ω = ⊥
Uses 2 · Used by 4
Statement usesLiminf of a random walk · Limsup of a random walk
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy on sequence space · Random-walk dichotomy, finite-limit form · Random-walk dichotomy

DefinitionRandom walk with a finite limit#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space \((\Omega, \mu)\) and \(S_n = \sum_{i < n} X_i\). The random walk \((S_n)\) converges to a finite limit if for \(\mu\)-almost every \(\omega\) there is \(l \in \mathbb{R}\) with \(S_n(\omega) \to l\) as \(n \to \infty\).

The limit may depend on \(\omega\); the zero-walk alternative of the i.i.d. random-walk dichotomy implies this property.

def ConvergesFinite {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) : Prop :=
  ∀ᵐ ω ∂μ, ∃ l : ℝ, Tendsto (fun n => randomWalkPartialSum X n ω) Filter.atTop
    (𝓝 l)
Uses 1 · Used by 3
Statement usesPartial sums of a random walk
Used byA zero walk converges to a finite limit · Random-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy, finite-limit form

TheoremA random walk is zero exactly when its steps are#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space and \(S_n = \sum_{i < n} X_i\). Then almost surely \(S_n = 0\) for every \(n\) if and only if almost surely \(X_i = 0\) for every \(i\).

theorem zeroWalk_iff_ae_forall_eq_zero {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} :
    ZeroWalk μ X ↔ ∀ᵐ ω ∂μ, ∀ i, X i ω = 0
Uses 2 · Used by 3
Statement usesZero random walk
Proof usesPartial sums of a random walk
Used byA zero walk converges to a finite limit · Random-walk dichotomy on sequence space · Random-walk dichotomy

TheoremA zero walk converges to a finite limit#✓fully proved

Let \(X_0, X_1, \dots\) be real random variables on a probability space and \(S_n = \sum_{i < n} X_i\). If almost surely \(S_n = 0\) for every \(n\), then almost surely there is \(l \in \mathbb{R}\) with \(S_n \to l\) as \(n \to \infty\).

theorem ZeroWalk.convergesFinite {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ}
    (h : ZeroWalk μ X) : ConvergesFinite μ X
Uses 4 · Used by 2
Statement usesRandom walk with a finite limit · Zero random walk
Proof usesVanishing steps give a convergent random walk · A random walk is zero exactly when its steps are
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy, finite-limit form

TheoremRandom-walk dichotomy on sequence space#✓fully proved

Let \(\rho\) be a probability measure on \(\mathbb{R}\), let \(\nu = \rho^{\otimes \mathbb{N}}\) be the product measure on \(\mathbb{R}^{\mathbb{N}}\), and let \(S_n(\omega) = \sum_{i < n} \omega_i\) be the partial sums of the coordinates. Then one of the following holds: \(\nu\)-almost surely \(S_n = 0\) for every \(n\); \(\nu\)-almost surely \(S_n \to +\infty\); \(\nu\)-almost surely \(S_n \to -\infty\); or \(\nu\)-almost surely \(\limsup_n S_n = +\infty\) and \(\liminf_n S_n = -\infty\).

theorem dichotomy_product_zero (ρ : Measure ℝ) [IsProbabilityMeasure ρ] :
    ZeroWalk (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    DriftsToTop (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    DriftsToBot (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    Oscillates (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq
Uses 19 · Used by 2
Statement usesRandom walk drifting to \(-\infty\) · Random walk drifting to \(+\infty\) · Oscillating random walk · Zero random walk · Coordinate process on sequence space
Proof usesHewitt–Savage zero–one law on a Polish space · Zero–one sublevel sets force an almost surely constant variable · Finite permutations do not change the liminf of the partial sums · One-step shift identity for the liminf of the partial sums · Finite permutations do not change the limsup of the partial sums · One-step shift identity for the limsup of partial sums · Shift invariance of the i.i.d. product measure · Liminf of a random walk · Limsup of a random walk · Shift of a real sequence · Limsup minus infinity forces divergence to minus infinity · Liminf plus infinity forces divergence to plus infinity · A random walk is zero exactly when its steps are · Partial sums of a random walk
Used byRandom-walk dichotomy on sequence space, finite-limit form · Random-walk dichotomy

TheoremRandom-walk dichotomy on sequence space, finite-limit form#✓fully proved

Let \(\rho\) be a probability measure on \(\mathbb{R}\), let \(\nu = \rho^{\otimes \mathbb{N}}\) be the product measure on \(\mathbb{R}^{\mathbb{N}}\), and let \(S_n(\omega) = \sum_{i < n} \omega_i\) be the partial sums of the coordinates. Then one of the following holds: \(\nu\)-almost surely \(S_n\) converges to a finite limit (which may depend on \(\omega\)); \(\nu\)-almost surely \(S_n \to +\infty\); \(\nu\)-almost surely \(S_n \to -\infty\); or \(\nu\)-almost surely \(\limsup_n S_n = +\infty\) and \(\liminf_n S_n = -\infty\).

theorem dichotomy_product (ρ : Measure ℝ) [IsProbabilityMeasure ρ] :
    ConvergesFinite (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    DriftsToTop (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    DriftsToBot (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq ∨
    Oscillates (Measure.infinitePi (fun _ : ℕ => ρ)) coordSeq
Uses 8
Statement usesRandom walk with a finite limit · Random walk drifting to \(-\infty\) · Random walk drifting to \(+\infty\) · Oscillating random walk · Coordinate process on sequence space
Proof usesZero random walk · A zero walk converges to a finite limit · Random-walk dichotomy on sequence space

TheoremRandom-walk dichotomy#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed real random variables on a probability space and \(S_n = \sum_{i < n} X_i\). Then one of the following events has probability one: \(S_n = 0\) for every \(n\); \(S_n \to +\infty\); \(S_n \to -\infty\); or \(\limsup_n S_n = +\infty\) and \(\liminf_n S_n = -\infty\).

theorem random_walk_dichotomy_zero {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ)
    (hindep : iIndepFun X μ) (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
    ZeroWalk μ X ∨ DriftsToTop μ X ∨ DriftsToBot μ X ∨ Oscillates μ X
Uses 13 · Used by 1
Statement usesRandom walk drifting to \(-\infty\) · Random walk drifting to \(+\infty\) · Oscillating random walk · Zero random walk
Proof usesCoordinate process on sequence space · Random-walk dichotomy on sequence space · The event of drift to \(-\infty\) on sequence space is measurable · The event of drift to \(+\infty\) on sequence space is measurable · The zero-sequence event is measurable · Liminf of a random walk · Limsup of a random walk · A random walk is zero exactly when its steps are · Partial sums of a random walk
Used byRandom-walk dichotomy, finite-limit form

TheoremRandom-walk dichotomy, finite-limit form#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed real random variables on a probability space and \(S_n = \sum_{i < n} X_i\). Then one of the following events has probability one: \(S_n\) converges to a finite limit (which may depend on the outcome); \(S_n \to +\infty\); \(S_n \to -\infty\); or \(\limsup_n S_n = +\infty\) and \(\liminf_n S_n = -\infty\).

theorem random_walk_dichotomy {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ)
    (hindep : iIndepFun X μ) (hident : ∀ i, IdentDistrib (X i) (X 0) μ μ) :
    ConvergesFinite μ X ∨ DriftsToTop μ X ∨ DriftsToBot μ X ∨ Oscillates μ X
Uses 7
Statement usesRandom walk with a finite limit · Random walk drifting to \(-\infty\) · Random walk drifting to \(+\infty\) · Oscillating random walk
Proof usesZero random walk · A zero walk converges to a finite limit · Random-walk dichotomy
52 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.