Documentation

BGW.Probability.RealWalkMaximal

Maximal inequalities for real iid walks #

This file defines finite-horizon exceedance probabilities and proves Ottaviani's maximal inequality using first-exit events and fresh-start independence.

Reference: P. Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Theorem 9.7 (Ottaviani's inequality).

source
def BGW.Probability.RealWalk.maxExceed (m : ℕ) (r : ℝ) :
Set (ℕ → ℝ)

The finite-horizon exceedance event {∃ k ≤ m, r < |S_k|}.

Equations
Instances For
    source
    theorem BGW.Probability.RealWalk.measurableSet_maxExceed (m : ℕ) (r : ℝ) :
    MeasurableSet (maxExceed m r)
    source
    noncomputable def BGW.Probability.RealWalk.maxTail (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) (r : ℝ) :
    ℝ

    maxTail ν m r = P(max_{k ≤ m} |S_k| > r): the genuine maximum probability, not a supremum of marginal probabilities.

    Equations
    Instances For
      source
      theorem BGW.Probability.RealWalk.maxTail_nonneg (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) (r : ℝ) :
      0 ≤ maxTail ν m r
      source
      theorem BGW.Probability.RealWalk.maxTail_le_one (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) (r : ℝ) :
      maxTail ν m r ≤ 1
      source
      theorem BGW.Probability.RealWalk.maxTail_mono_length (ν : MeasureTheory.ProbabilityMeasure ℝ) {m m' : ℕ} (h : m ≤ m') (r : ℝ) :
      maxTail ν m r ≤ maxTail ν m' r

      Monotone in the length.

      source
      theorem BGW.Probability.RealWalk.maxTail_anti_threshold (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) {r r' : ℝ} (h : r ≤ r') :
      maxTail ν m r' ≤ maxTail ν m r

      Antitone in the threshold.

      source
      theorem BGW.Probability.RealWalk.measureReal_exceed_block (ν : MeasureTheory.ProbabilityMeasure ℝ) (a m : ℕ) (r : ℝ) :
      (↑(iidLaw ν)).real {ω : ℕ → ℝ | ∃ k ≤ m, r < |blockSum ω a k|} = maxTail ν m r

      Block translation: the maximum of |S_{a+k} - S_a|, k ≤ m, has the same exceedance probability as the walk started at 0 (fresh start at the deterministic index a).

      source
      theorem BGW.Probability.RealWalk.maximal_le_two_mul_tail (ν : MeasureTheory.ProbabilityMeasure ℝ) (m : ℕ) (r : ℝ) (hsafe : ∀ j ≤ m, 1 / 2 ≤ (↑(sumLaw ν j)).real {x : ℝ | |x| ≤ r}) :
      maxTail ν m (2 * r) ≤ 2 * (↑(sumLaw ν m)).real {x : ℝ | r < |x|}

      Ottaviani's maximal inequality for real iid sums (Node 6). If every partial sum S_j, j ≤ m, lies in [-r, r] with probability ≥ 1/2 (the "safe remainder" hypothesis, applied to the independent remainder S_m - S_k of length m - k ≤ m), then P(max_{k ≤ m} |S_k| > 2 r) ≤ 2 P(|S_m| > r).