The heat inequality in affine parabolic coordinates

The differential inequality in thm:bu is preserved on the normalized half-space cylinder by subunit affine parabolic changes of variables.

theorem ESS.bu_affine_weak_heat (τ 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 (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw) z = scale ^ 2 • ucWeakHeatVector D2w Dtw (buAffinePoint τ scale z)

The weak heat vector scales by two spatial powers in affine parabolic coordinates.

theorem ESS.bu_affine_gradient_sq (τ 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 (buAffineField τ scale w) (buAffineDw τ scale Dw) z = scale ^ 2 * CKN.spatialGradientSq w Dw (buAffinePoint τ scale z)

The squared first spatial derivative scales by two spatial powers.

theorem ESS.bu_affine_weak_heat_bound (τ 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₁ * (√(CKN.spatialGradientSq (buAffineField τ scale w) (buAffineDw τ scale Dw) z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField τ scale w z))

A pointwise weak heat inequality keeps the same coefficient after a subunit affine parabolic change of variables.

theorem ESS.bu_affine_ae_pullback (τ scale : ℝ) (hscale : 0 < scale) (P : CKN.Foundation.Parabolic.ParabolicPoint → Prop) (hP : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo τ (τ + scale ^ 2))), P z) : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), P (buAffinePoint τ scale z)

Almost everywhere statements pull back through the affine parabolic map on the positive half-space slab.

theorem ESS.bu_affine_weak_heat_ae_bound (τ scale c₁ : ℝ) (hτ : 0 ≤ τ) (hscale : 0 < scale) (hupper : τ + scale ^ 2 ≤ 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) (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 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buAffineD2w τ scale D2w) (buAffineDtw τ scale Dtw) z) ≤ c₁ * (√(CKN.spatialGradientSq (buAffineField τ scale w) (buAffineDw τ scale Dw) z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (buAffineField τ scale w z))

The almost everywhere differential inequality in thm:bu transfers through a subunit affine parabolic change of variables.