Gaussian fourth moment by scaling in Lean, and quadratic variation of Brownian motion

To get E[X^4] for X ~ gaussianReal 0 v without computing 3v^2: rewrite gaussianReal 0 v as (gaussianReal 0 1).map (sqrt v * ·) using gaussianReal_map_const_mul (μ := 0) (v := 1) (sqrt v). The NNReal parameter is NNReal.mk (sqrt v ^ 2) _ * 1; close it with rw [h, mul_zero]; congr 1; ext; simp. A direct rw with a hand-written ⟨_, _⟩ * 1 = v failed to match. Then integral_map (by fun_prop) (by fun_prop), mul_pow, integral_const_mul. Use Real.sq_sqrt explicitly; with open Real the bare sq_sqrt v.2 did not rewrite. Transfer to a random variable with HasLaw.integral_comp. MemLp (X^2) 2: (hX.hasSubgaussianMGF_gaussianReal).memLp 4, then MemLp.integrable_norm_pow and memLp_two_iff_integrable_sq. With IndepFun.variance_sum, variance_le_expectation_sq, meas_ge_le_variance_div_sq and ae_eventually_notMem, Levy's dyadic quadratic variation theorem for IsPreBrownianReal needs neither continuity nor measurability of B t.