Theorem 2.17 -- avoiding zero for $r$ steps

Open

MarkovMixing.srw_zero_avoidance

by Shuze Chen · Aug 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmixing-timesprobability

For simple random walk on $\mathbb{Z}$ started at $k>0$ , the probability of not visiting $0$ within $r$ steps is at most

\mathbb{P}_k\{\tau_0>r\}\le\frac{12k}{\sqrt r}.

The probability is the exact fraction of the $2^r$ sign strings whose walk avoids $0$ at all times $t\le r$ .

Preamble

import Definitions.Def_mm_classical

Formal statement

namespace MarkovMixing

/-- **Theorem 2.17** (LPW): for simple random walk on `ℤ` started at `k > 0`,
the probability of not visiting `0` within `r` steps is at most `12k/√r`. -/
theorem srw_zero_avoidance (r : ℕ) (hr : 0 < r) (k : ℤ) (hk : 0 < k) :
    ((Finset.univ.filter fun ω : Fin r → Bool =>
        ∀ t ≤ r, srwPos k ω t ≠ 0).card : ℝ) / 2 ^ r ≤
      12 * (k : ℝ) / Real.sqrt r := by
  sorry

end MarkovMixing

Source

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, AMS 2009, https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf, Section 2.7, Theorem 2.17, p. 30

Read-back

What the Lean code literally says, in plain math · claude-fable-5

For every natural number $r$ with $0 < r$ and every integer $k$ with $0 < k$ , the theorem asserts the following inequality of real numbers. For a sign sequence $\omega \in \{\pm 1\}^r$ (formally a function from $\{0,\dots,r-1\}$ to Booleans, with "true" read as $+1$ and "false" as $-1$ ) and a natural number $t$ , define the walk position at time $t$ started from $k$ as

S_t(\omega) \;=\; k + \sum_{i=0}^{r-1} \begin{cases} \pm 1 & \text{if } i < t \text{ (sign given by } \omega_i\text{)}\\ 0 & \text{otherwise,}\end{cases}

i.e. $S_t(\omega) = k + \sum_{i < \min(t,r)} \omega_i$ , an integer; in particular $S_0(\omega) = k$ , and for $t \ge r$ the value is frozen at $S_r(\omega)$ . Let $N$ be the number of sign sequences $\omega \in \{\pm 1\}^r$ such that $S_t(\omega) \ne 0$ for every natural number $t$ with $t \le r$ — that is, the walk started at $k$ avoids $0$ at all of the $r+1$ time points $t = 0, 1, \dots, r$ (the condition at $t = 0$ reads $k \ne 0$ , which is automatic since $k > 0$ ). The theorem then claims

\frac{N}{2^{r}} \;\le\; \frac{12\,k}{\sqrt{r}},

where $N$ and $k$ are cast to real numbers, $2^r$ is a real power, and $\sqrt{r}$ is the real square root of $r$ (positive, since $r \ge 1$ , so the right-hand side is a well-defined positive real). Equivalently, the left-hand side is the probability, under the uniform distribution on the $2^r$ sign sequences, that the $\pm 1$ walk started at height $k$ never touches $0$ during its first $r$ steps. Note that the right-hand side $12k/\sqrt{r}$ can exceed $1$ (e.g. whenever $r \le 144\,k^2$ ), in which case the inequality holds trivially because the left-hand side is a probability in $[0,1]$ ; the bound carries content only for $r$ large relative to $k^2$ . The inequality is an upper bound only (a claim that the avoidance probability is small, with no matching lower bound), it is non-strict ( $\le$ ), and no assumption relates $k$ to $r$ beyond $r \ge 1$ and $k \ge 1$ .

Human review

Endorsed by Community (Bot) · Aug 21, 2026
Endorsed by Shuze Chen · Aug 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 2.17 -- avoiding zero for rrr steps

Theorem 2.17 -- avoiding zero for $r$ steps