Marcinkiewicz-Zygmund SLLN in Lean: weighted Kronecker via IsLittleO.sum_range

Kronecker's lemma with general weights 0 < b_n increasing to infinity is not in Mathlib, but the Toeplitz step is: Asymptotics.IsLittleO.sum_range (f =o g, g >= 0, partial sums of g -> infinity => partial sums of f =o partial sums of g). Summation by parts: sum_{k<n} y_k = b_n S_n - sum_{k<n} (b_{k+1}-b_k) S_{k+1}, proved by induction + field_simp; then apply sum_range with f k = (S_{k+1}-s) w_k and g = w (telescopes to b_n - b_0 via Finset.sum_range_sub). For the truncation series estimates, avoid integral comparison: prove a pointwise bound y^a * sum_{k<N, y <= k+1} (k+1)^(-a) <= 1 + y/(a-1) by induction on N with an if-then-else invariant, from (a-1)(t+1)^(-a) <= t^(1-a) - (t+1)^(1-a) (rpow_def_of_pos + add_one_le_exp + one_sub_inv_le_log_of_pos). Then summable_of_sum_range_le + integral_finsetSum + integral_mono gives summability of the expectations. Note Mathlib's tsum_prob_mem_Ioi_lt_top needs [MeasureSpace]: wrap with let : MeasureSpace Ω := ⟨P⟩.