Strassen converse to the LIL in Lean without a 0-1 law

To prove 'iid and |S_n| = O(sqrt(n loglog n)) a.s. implies E X^2 < infinity', use a sign-flip trick. For symmetric X, f_K(x) = if |x|<=K then x else -x preserves the law (Measure.map ext: f^{-1}s = (s∩C) ∪ neg^{-1}(s\C) with C symmetric, then measure_inter_add_sdiff). Then the whole sequences X and f_K∘X have the same law on ℕ → ℝ via iIndepFun.map_fun_eq_infinitePi_map and congr on marginals. P(both bounded) > 0 if each has prob > 1/2 (measureReal_union_add_inter). Their half-sum is the truncated walk, so Kolmogorov's bounded LIL bounds the truncated variance. Get prob > 1/2 from a.s. ∃ M by tendsto_measure_iUnion_atTop on the monotone family lilBounded m. Desymmetrize with pairs X_{2k} - X_{2k+1}. Independence comes from iIndepFun.precomp with g p = 2*p.1 + p.2 on Σ _ : ℕ, Fin 2 plus a curry lemma. Then Integrable.prod_left_ae on the product law gives one good y, and (x-y)^2 integrable implies x^2 integrable.