Pointwise heat bound for a scalar cutoff

The weak heat operator of a scalar cutoff field is bounded by the scaled equation and the first and second cutoff derivatives.

theorem ESS.buCut_heat_error_le (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (M : ℝ) (hM : 0 ≤ M) (hderiv : ∀ (j : Fin 3), |CKN.spatialPartial (buCutScalar κ) j z| ≤ M) : CKN.Foundation.Parabolic.vec3EuclideanNorm (buCutHeatError κ v Dv z) ≤ |CKN.timePartial (buCutScalar κ) z + ∑ j : Fin 3, CKN.spatialSecondPartial (buCutScalar κ) j j z| * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * M * √(CKN.spatialGradientSq v Dv z)

The cutoff error in the weak heat operator is bounded by the scalar heat derivative and the spatial gradient of the cutoff.

theorem ESS.buCut_heat_le (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (c : ℝ) (hc : 0 ≤ c) (hκ : 0 ≤ buCutScalar κ z) (M : ℝ) (hM : 0 ≤ M) (hderiv : ∀ (j : Fin 3), |CKN.spatialPartial (buCutScalar κ) j z| ≤ M) (hheat : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (√(CKN.spatialGradientSq v Dv z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (v z))) : CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector (buCutD2 κ v Dv D2v) (buCutDt κ v Dtv) z) ≤ c * (CKN.Foundation.Parabolic.vec3EuclideanNorm (buCutField κ v z) + 3 * √(CKN.spatialGradientSq (buCutField κ v) (buCutDw κ v Dv) z)) + (3 * c * M + |CKN.timePartial (buCutScalar κ) z + ∑ j : Fin 3, CKN.spatialSecondPartial (buCutScalar κ) j j z|) * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + 18 * M * √(CKN.spatialGradientSq v Dv z)

The scaled heat inequality passes to a scalar cutoff field with an explicit cutoff-derivative error.