Proving sup Sₙ = ∞ a.s. for a random walk without iid ladder heights: Laplace-weight the 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).