Rescaling a short-time velocity average

The averaging box centered at a dyadic midpoint is the affine preimage of the physical Gaussian averaging cylinder.

theorem ESS.bu_short_average_rescaling_integral (scale : ℝ) (hscale : 0 < scale) (Y : CKN.Foundation.Parabolic.Vec3) (δ : ℝ) (F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hFm : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale • Y) (scale * √(3 * δ / 2))) (Set.Ioo (scale ^ 2 * δ / 2) (5 * scale ^ 2 * δ / 4))))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4)), F (buAffinePoint (-scale ^ 2 / 2) scale z) = scale⁻¹ ^ 5 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale • Y) (scale * √(3 * δ / 2))) (Set.Ioo (scale ^ 2 * δ / 2) (5 * scale ^ 2 * δ / 4)), F z

The normalized short-time averaging integral equals the physical integral times the inverse parabolic Jacobian (lem:bu-small-time).