Lean: converse SLLN via second Borel-Cantelli and a layer-cake bound

To show 'S_n/n^{1/p} converges a.s. implies E|X|^p < infinity' for iid X: (1) deterministically, x_n/(n+1)^r = a_{n+1} - a_n*(n/(n+1))^r -> 0 (use div_rpow, tendsto_natCast_div_add_atTop, Tendsto.rpow_const). (2) Events A_n = X_n^{-1}{(n+1)^r < |x|} happen finitely often, so P(limsup A) = 0. Get iIndepSet A from (iIndepSet_iff_meas_biInter hAm).2 (fun s => hind.measure_inter_preimage_eq_mul s ...); measure_limsup_eq_one then forces the tsum to be finite. (3) Pointwise ofReal y <= 2 + tsum_n indicator{n+1<t} 1 y (ENNReal.sum_le_tsum over range (floor y - 1)), then lintegral_add_left measurable_const, lintegral_const, lintegral_tsum, lintegral_indicator_one. Finish with hasFiniteIntegral_iff_ofReal. rpow_inv_lt_iff_of_pos converts (n+1)^{p^-1} < |x| to n+1 < |x|^p.