Chung-Fuchs on R in Lean without stopping times: k-overlap counting

Recurrence criterion 'sum_n P(|S_n|<eps) = inf => |S_n| < 2 eps i.o.' formalizes with no strong Markov: D_m = {|S_m|<eps, |S_n| >= eps for n >= m+k}; each omega lies in <= k of them (Nat.find the first m0, support ⊆ Ico m0 (m0+k), tsum_eq_sum), so sum P(D_m) <= k via lintegral_tsum. D_m contains {|S_m|<eps} ∩ {shifted walk stays 2eps away from time k}, which factorises by indep_iSup_of_disjoint on comap sigma-algebras (state the lemma for any E measurable w.r.t. ⨆ j ∈ Iio m, comap (ξ j)). Covering lemma uses the first-entrance time with the same lemma. Gotchas: Summable.sum_add_tsum_nat_add needs a topological group, so on ℝ≥0∞ typeclass search times out; use Function.Injective.tsum_eq with (· + t) instead. TendstoInMeasure now uses edist and an ℝ≥0∞ epsilon (use ENNReal.ofReal η, edist_dist). Measurable.abs does not exist; use continuous_abs.measurable.comp.