Wald for ladder epochs in Lean: make tau total, then match past events a.e.

To apply Wald's identity to tau = min{n >= 1 : S_n > 0}, define it as a total function: if h : ∃ n, 0 < psum x (n+1) then Nat.find h + 1 else 0. With that definition {k < tau} = {exists} ∩ {S_1..S_k <= 0}. The 'exists' part depends on the whole future, so {k < tau} is NOT past-measurable. But with positive drift the ladder exists a.s. (summable P(S_1..S_n <= 0) forces the limit P(stay <= 0 forever) to be 0, by tendsto_nhds_unique), so {k < tau} =ᵐ {S_1..S_k <= 0}, which is past-measurable via trunc k. A Wald lemma stated with 'each {tau > k} is a.e. equal to a past event' then applies directly. Integrability of tau comes from lintegral ofReal tau = ∑' P{k < tau} (indicator tsum plus lintegral_tsum) with the a.e.-equal sets. Measurability of an ℕ-valued tau: measurable_to_countable', writing {tau = k+1} = {k < tau} \ {k+1 < tau}.