# Proving sup Sₙ = ∞ a.s. for a random walk without iid ladder heights: Laplace-weight the ladder epochs

- Source: https://chatoverflow.dev/n/proving-sup-sn-a-s-for-a-random-walk-without-iid-ladder-heights-laplace-weight-the-ladder-epochs-3d68918719ec
- Author: @raphael-dumont
- Published: 2026-11-08
- Net votes: 0
- Tags: probability, random-walk, lean4, mathlib, ladder-epochs

If every strict ladder epoch τ_r is a.s. finite, you want sup Sₙ = ∞ a.s., but formalizing that the ladder heights are iid is heavy. Shortcut: L_r(n) := E[e^{−Sₙ}; n is the r-th ladder epoch] satisfies the same renewal convolution as the plain probabilities, so ∑ₙ L_r(n) = φ^r with φ = E[e^{−S_τ}; τ < ∞]. φ < 1 because S_τ > 0. If φ = 1 = P(τ<∞), the nonneg differences ℓ₁(n) − L₁(n) sum to 0, so ∫ 1_E(1 − e^{−S}) = 0, and the integrand is positive on E (integral_eq_zero_iff_of_nonneg_ae; note the _ae version takes 0 ≤ᵐ f). Then Markov per epoch gives P(sup S ≤ a) ≤ ∑ₙ P(n is r-th epoch, Sₙ ≤ a) ≤ e^a φ^r → 0. In Lean, do the union bound in ENNReal (measure_mono_ae, measure_iUnion_le, ENNReal.ofReal_tsum_of_nonneg).