Integrals under the Gaussian parabolic dilation #
The affine map in lem:uc-gaussian carries the normalized cylinder onto
the corresponding source cylinder.
theorem
ESS.uc_scaled_box_preimage
(x₀ : CKN.Foundation.Parabolic.Vec3)
(scale r s : ℝ)
(hscale : 0 < scale)
:
CKN.spaceTimeSet (CKN.rescaledSpace scale x₀ (CKN.Foundation.Parabolic.vec3Ball x₀ (scale * r)))
(CKN.rescaledTime scale 0 (Set.Ioo 0 (scale ^ 2 * s))) = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 r) (Set.Ioo 0 s)
A parabolic box is the preimage of its translated, dilated box.
theorem
ESS.uc_scaled_cylinder_preimage
(x₀ : CKN.Foundation.Parabolic.Vec3)
(scale ρ : ℝ)
(hscale : 0 < scale)
:
CKN.spaceTimeSet (CKN.rescaledSpace scale x₀ (CKN.Foundation.Parabolic.vec3Ball x₀ (scale * ρ)))
(CKN.rescaledTime scale 0 (Set.Ioo 0 (scale ^ 2 * 2))) = ucCylinder ρ
The normalized Gaussian cylinder is the preimage of its translated, dilated source cylinder.
theorem
ESS.uc_gaussian_energy_rescaling
(R T scale ρ : ℝ)
(hR : 0 < R)
(hT : 0 < T)
(hscale : 0 < scale)
(hball : scale * ρ ≤ 3 * R / 4)
(htime : 2 * scale ^ 2 ≤ 3 * T / 4)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(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)
(hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T) w Dw D2w Dtw)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 < ⊤)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, CKN.Foundation.Parabolic.vec3EuclideanNorm (ucScaledField x₀ scale w z) ^ 2 + CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z ≤ 2 * scale.rpow (-5) * ucLocalEnergy x₀ R T w Dw
The normalized cylinder energy is controlled by the source energy after
parabolic dilation (lem:uc-gaussian).