Derivative data under parabolic scaling

The weak derivative fields of lem:uc-gaussian transform with one or two powers of the spatial scale.

theorem ESS.uc_scaled_weak_heat (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ucWeakHeatVector (ucScaledD2w x₀ scale D2w) (ucScaledDtw x₀ scale Dtw) z = scale ^ 2 • ucWeakHeatVector D2w Dtw (ucScaledPoint x₀ scale z)

The specified weak heat vector scales by the square of the parabolic spatial scale.

theorem ESS.uc_scaled_gradient_sq (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialGradientSq (ucScaledField x₀ scale w) (ucScaledDw x₀ scale Dw) z = scale ^ 2 * CKN.spatialGradientSq w Dw (ucScaledPoint x₀ scale z)

The squared spatial gradient scales by the square of the spatial scale.

theorem ESS.uc_scaled_weak_heat_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) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hineq : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw (ucScaledPoint x₀ scale z)) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w (ucScaledPoint x₀ scale z)) + √(CKN.spatialGradientSq w Dw (ucScaledPoint x₀ scale z)))) : 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 keeps its form under a subunit parabolic scale, with coefficient multiplied by that scale.