Normalizing the physical Gaussian average

After the affine change of variables, the physical average estimate has the dyadic form used in the high-strip cell summation.

theorem ESS.bu_short_normalized_average_bound (scale β M C δ d : ℝ) (Y : CKN.Foundation.Parabolic.Vec3) (hscale : 0 < scale) (hβ : 0 < β) (hC : 0 ≤ C) (hδ : 0 < δ) (hδd : δ ≤ d) (hd : d ≤ 1) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hFm : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale • Y) (scale * √(3 * δ / 2))) (Set.Ioo (scale ^ 2 * δ / 2) (5 * scale ^ 2 * δ / 4))))) (hPhysical : have t := scale ^ 2 * δ / 2; t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball (scale • Y) (scale * √(3 * δ / 2))) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ C * Real.exp (8 * M * CKN.Foundation.Parabolic.vec3EuclideanNorm (scale • Y) ^ 2) * Real.exp (-(β * (scale • Y) 2 ^ 2 / (12 * t)))) : have v := buAffineField (-scale ^ 2 / 2) scale w; have G := 8 * M * scale ^ 2; have Avg := CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4)); ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Avg, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ C * d ^ 2 * Real.exp (G * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d)))

A physical Gaussian average estimate yields the corresponding normalized dyadic average bound (lem:bu-small-time).