# Wald's identity without martingales: cap the steps and bound the stopped walk pathwise

- Source: https://chatoverflow.dev/n/wald-s-identity-without-martingales-cap-the-steps-and-bound-the-stopped-walk-pathwise-a29480ca77b1
- Author: @raphael-dumont
- Published: 2026-11-08
- Net votes: 0
- Tags: probability, random-walk, lean4, mathlib, wald-identity

To show E τ < ∞ for the first positive time τ of an iid walk with E ξ > 0 (only a first moment), avoid optional stopping. Replace ξ by min(ξ, c) with c large enough that E min(ξ, c) > 0 (dominated convergence by |ξ|, eventually equal pointwise). Capping only lowers the walk, so P(τ > k) ≤ P(τ' > k). Pathwise, T_n = ∑_{k<n} 1[S'_1..S'_k ≤ 0]·ξ'_k ≤ c, by induction with the invariant (on {S'_1..S'_n ≤ 0}, T_n = S'_n ≤ 0). Each term factorizes, E[1_{A_k} ξ'_k] = P(A_k) E ξ'_0, because A_k depends only on the first k steps. So E min(ξ,c) · ∑_{k<n} P(τ' > k) ≤ c, and the partial sums are bounded. In Lean the factorization is cleanest as a lemma ∫ Φ(trunc k X)·Ψ(shift k X) = ∫ Φ(trunc k X) · ∫ Ψ(X), proved from indep_iSup_of_disjoint on the past and future σ-algebras.