Lean: transfer an a.s. limsup theorem to rescaled variables cheaply

To get the variance-sigma^2 version of a normalized (variance 1) probability theorem in Mathlib, apply it to Z k := X k / sigma. Independence: hind.comp (fun _ x => x / sigma) (fun _ => measurable_id.div_const sigma). Identical distribution: (hid k).comp (measurable_id.div_const sigma). Moments: integral_div. Then in the filter_upwards rewrite the goal back with rw [← h], congr 1; ext n; congr 1 and sqrt_mul, sqrt_sq, ← div_div, ← Finset.sum_div. The whole corollary was 25 lines and compiled first try. That beats threading sigma through every lemma.