Law of the iterated logarithm

TheoremLaw of the iterated logarithm, square-integrable form#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed, measurable real random variables on a probability space with \(\mathbb{E}[X_0^2] < \infty\), \(\mathbb{E}[X_0] = 0\) and \(\operatorname{Var}(X_0) = 1\), and let \(S_n = X_0 + \dots + X_{n-1}\). Then almost surely \(\limsup_{n \to \infty} S_n / \sqrt{2 n \log \log n} = 1\) and \(\liminf_{n \to \infty} S_n / \sqrt{2 n \log \log n} = -1\).

Integrability of \(X_0\) is not assumed separately, since it follows from square integrability on a probability space.

MathlibExt.Probability.LawIteratedLogarithmWanted.law_of_the_iterated_logarithm_of_memLp · 16 lines

public theorem law_of_the_iterated_logarithm_of_memLp
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : ℕ → Ω → ℝ)
    (hMeas : ∀ n, Measurable (X n))
    (hIndep : iIndepFun X μ)
    (hIdent : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    (hMemLp : MemLp (X 0) 2 μ)
    (hMean : μ[X 0] = 0)
    (hVar : Var[X 0; μ] = 1) :
    ∀ᵐ ω ∂μ,
      Filter.limsup (fun n : ℕ =>
        (∑ i ∈ Finset.range n, X i ω) /
          Real.sqrt (2 * (n : ℝ) * Real.log (Real.log (n : ℝ)))) Filter.atTop = (1 : ℝ)
      ∧ Filter.liminf (fun n : ℕ =>
        (∑ i ∈ Finset.range n, X i ω) /
          Real.sqrt (2 * (n : ℝ) * Real.log (Real.log (n : ℝ)))) Filter.atTop = (-1 : ℝ)

Used by 1

Used byLaw of the iterated logarithm

TheoremLaw of the iterated logarithm#✓fully proved

Let \(X_0, X_1, \dots\) be independent, identically distributed, measurable real random variables on a probability space such that \(X_0\) is integrable, \(\mathbb{E}[X_0^2] < \infty\), \(\mathbb{E}[X_0] = 0\) and \(\operatorname{Var}(X_0) = 1\), and let \(S_n = X_0 + \dots + X_{n-1}\). Then almost surely \(\limsup_{n \to \infty} S_n / \sqrt{2 n \log \log n} = 1\) and \(\liminf_{n \to \infty} S_n / \sqrt{2 n \log \log n} = -1\).

Proof: Hartman–Wintner truncation and exponential maximal bounds give the upper half; a CLT block argument and the second Borel–Cantelli lemma give the lower half.

MathlibExt.Probability.LawIteratedLogarithmWanted.law_of_the_iterated_logarithm · 17 lines

public theorem law_of_the_iterated_logarithm
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    (X : ℕ → Ω → ℝ)
    (hMeas : ∀ n, Measurable (X n))
    (hIndep : iIndepFun X μ)
    (hIdent : ∀ i, IdentDistrib (X i) (X 0) μ μ)
    (hInt : Integrable (X 0) μ)
    (hMemLp : MemLp (X 0) 2 μ)
    (hMean : μ[X 0] = 0)
    (hVar : Var[X 0; μ] = 1) :
    ∀ᵐ ω ∂μ,
      Filter.limsup (fun n : ℕ =>
        (∑ i ∈ Finset.range n, X i ω) /
          Real.sqrt (2 * (n : ℝ) * Real.log (Real.log (n : ℝ)))) Filter.atTop = (1 : ℝ)
      ∧ Filter.liminf (fun n : ℕ =>
        (∑ i ∈ Finset.range n, X i ω) /
          Real.sqrt (2 * (n : ℝ) * Real.log (Real.log (n : ℝ)))) Filter.atTop = (-1 : ℝ)

Sources

• A. Y. Khinchin 1924, A. N. Kolmogorov 1929, P. Hartman and A. Wintner, On the law of the iterated logarithm, Amer. J. Math. 63 (1941) 169–176; textbook in Durrett, Probability Theory and Examples, 5th ed., Foundations of Modern Probability (Hartman-Wintner LIL). Lean i.i.d. mean-zero variance-one normalized √(2 n log log n) form.

Uses 1

Proof usesLaw of the iterated logarithm, square-integrable form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.