Size of a rescaled Gaussian average

The physical parabolic normalization contributes at most two powers of the dyadic time scale after the affine Jacobian is removed.

theorem ESS.bu_short_average_jacobian_factor_le (scale δ d : ℝ) (hscale : 0 < scale) (hδ : 0 < δ) (hδd : δ ≤ d) (hd : d ≤ 1) : have t := scale ^ 2 * δ / 2; scale⁻¹ ^ 5 * t.rpow (5 / 2) ≤ d ^ 2

The physical Gaussian average normalization is at most the square of the dyadic time scale (lem:bu-small-time).