Heat inequality after shifting the initial time

The short-time parabolic change of variables reduces the coefficient in the weak heat inequality by its spatial scale.

theorem ESS.bu_affine_weak_heat_bound_scaled (τ 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 (buAffinePoint τ scale z)) ≤ c₁ * (√(CKN.spatialGradientSq w Dw (buAffinePoint τ scale z)) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w (buAffinePoint τ scale z)))) : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw) z) ≤ c₁ * scale * (√(CKN.spatialGradientSq (buAffineField τ scale w) (buAffineDw τ scale Dw) z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField τ scale w z))

The coefficient in the weak heat inequality gains one factor of the spatial scale under an affine parabolic change of variables.

theorem ESS.bu_affine_weak_heat_ae_bound_interval (τ scale a b c₁ : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hc₁ : 0 ≤ c₁) (hsource : Set.Ioo (τ + scale ^ 2 * a) (τ + scale ^ 2 * b) ⊆ Set.Ioo 0 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) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo a b)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw) z) ≤ c₁ * scale * (√(CKN.spatialGradientSq (buAffineField τ scale w) (buAffineDw τ scale Dw) z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField τ scale w z))

The weak heat inequality on an initial physical interval transfers to the shifted normalized interval with the scaled coefficient.