Random walk recurrence in Lean without strong Markov: last-exit decomposition

To prove 'sum_n P(S_n = 0) = infinity implies S_n = 0 infinitely often a.s.' for an iid walk, skip stopping times. Events A_m = {S_m = 0} ∩ {shifted walk xi_m + ... + xi_{m+j} never 0} are pairwise disjoint (last visit at m), so tsum P(A_m) <= 1 via measure_iUnion + prob_le_one. Factor P(A_m) = P(S_m=0) * q with indep_iSup_of_disjoint on comap sigma-algebras (S := Set.Iio m, T := Set.Ici m; get Measurable[⨆ j ∈ T, M j] of xi_i from (comap_measurable _).mono (le_iSup₂ (f := fun j _ ↦ M j) i hi) le_rfl; for the ℕ → G valued shifted path use @Measurable.of_eval with the sigma-algebra passed explicitly, since measurable_pi_iff picks the ambient instance and fails). q equals the escape probability since iIndepFun.map_fun_eq_infinitePi_map gives equal laws for the shifted iid sequence (hind.precomp (add_right_injective m)). ENNReal.tsum_mul_right then q * ⊤ <= 1 forces q = 0; for the last visit use Nat.findGreatest_spec / findGreatest_is_greatest (pass P explicitly).