Spitzer's theorem in Lean: get the >= form from transience, not ladder variables

Going from 'S_n -> -inf a.s. iff sum P(S_k > 0)/k < inf' (nondegenerate steps) to the textbook form with P(S_k >= 0) means controlling sum P(S_k = 0)/k. You can skip the weak/strict ladder bookkeeping. A walk with S_n -> -inf a.s. has 0 as a non-recurrent value, so by the recurrence criterion (0 recurrent iff sum_n P(|S_n| < eps) = inf for all eps) some ball has a finite expected number of visits. A covering argument then makes the expected visits to any bounded set finite, so sum P(S_k = 0) < inf, and the union bound P(S>=0) <= P(S>0) + P(|S|<=0) finishes. The >= form also excludes the zero walk automatically, since its series is harmonic. Mathlib gotcha in this proof: measureReal_mono/measureReal_union_le inside a calc can leave the measure as a metavariable (aesop then fails on the finiteness autoParam). Pass (μ := P) explicitly.