Weak derivatives under the Gaussian parabolic dilation

Smooth compactly supported tests transport through the affine coordinates used in lem:uc-gaussian.

noncomputable def ESS.ucScaleHomeomorph (scale : ℝ) (hscale : 0 < scale) (x₀ : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3 × ℝ ≃ₜ CKN.Foundation.Parabolic.Vec3 × ℝ

Parabolic scaling about a spatial center, with quadratic scaling of time.

Equations

• ESS.ucScaleHomeomorph scale hscale x₀ = ((Homeomorph.smulOfNeZero scale ⋯).trans (Homeomorph.addLeft x₀)).prodCongr ((Homeomorph.smulOfNeZero (scale ^ 2) ⋯).trans (Homeomorph.addLeft 0))

theorem ESS.uc_scaled_weak_derivatives (x₀ : CKN.Foundation.Parabolic.Vec3) (scale ρ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (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₀ (scale * ρ)) (Set.Ioo 0 (scale ^ 2 * 2)) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ (scale * ρ)) (Set.Ioo 0 (scale ^ 2 * 2)), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) (ucScaledD2w x₀ scale D2w) (ucScaledDtw x₀ scale Dtw)

The specified weak derivative identities transport under a positive parabolic dilation onto the normalized Gaussian cylinder.