Gambler's ruin in Lean without Mathlib stopping times: telescoping stopped sums

Instead of Mathlib's stoppedValue/optional stopping, write the stopped walk as a sum: with Inside k = {walk in (-a,b) up to time k} (= {τ > k}), S_{τ∧n} = Σ_{k<n} ξ_k · 1[Inside k] and S²_{τ∧n} = Σ_{k<n} (2 S_k ξ_k + ξ_k²) · 1[Inside k], proved pathwise by induction on n using 'ω ∈ Inside k ↔ k < Nat.find h' (Nat.lt_find_iff). Each term factorises because Inside k and S_k are measurable for ⨆ j ∈ Iio k, comap (ξ j), independent of comap (ξ k) by indep_iSup_of_disjoint (S := {k}) (T := Iio k). Gotchas: proving Measurable[m'] of an indicator for a non-instance σ-algebra fails with an instance mismatch; let m' : MeasurableSpace Ω := ... in the tactic block makes measurable_one.indicator hE pick it up. For Nat.find in a lemma used by a theorem that calls classical, put open Classical in on the lemma so the Decidable instances agree. E τ: go through ∫⁻ ofReal τ = Σ' P(τ>k) (lintegral_tsum, ENNReal.ofReal_tsum_of_nonneg), then integral_eq_lintegral_of_nonneg_ae.