Differential inequality under parabolic scaling

The almost-everywhere heat inequality in lem:uc-gaussian transfers through the normalized parabolic coordinates.

theorem ESS.uc_scaled_weak_heat_ae_bound (x₀ : CKN.Foundation.Parabolic.Vec3) (scale ρ c₁ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hc₁ : 0 ≤ c₁) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsource : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ (scale * ρ)) (Set.Ioo 0 (scale ^ 2 * 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (ucScaledD2w x₀ scale D2w) (ucScaledDtw x₀ scale Dtw) z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) + √(CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z))

The differential inequality is preserved almost everywhere under the subunit parabolic dilation.