Integrated cutoff heat inequality #
The normalized weak heat inequality separates into an absorbable cutoff energy, an exponentially damped collar error, and an initial time error.
theorem
ESS.uc_cutoff_operator_integral_le
{ρ ε c₁ scale : ℝ}
(hρ : 4 ≤ ρ)
(hε : 0 < ε)
(hc₁ : 0 ≤ c₁)
(hscale : 0 ≤ scale)
{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}
(hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dv D2v Dtv)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z)))
:
have a := 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)));
have A := 32 + 3 * (CKN.cutoffSecondDerivativeConstant / ρ ^ 2) + 3 * c₁ * scale * (CKN.cutoffGradientConstant / ρ);
have B := 18 * (CKN.cutoffGradientConstant / ρ);
have Z := ucCutoffField (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v;
have DZ := ucCutoffDw (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv;
have LZ := ucCutoffHeat (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (LZ z) ^ 2 ≤ ((54 * (c₁ * scale) ^ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2 + CKN.spatialGradientSq Z DZ z)) + ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * (3 * (if z ∈ ucCutoffRegion ρ then
A * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + B * √(CKN.spatialGradientSq v Dv z)
else 0) ^ 2)) + 192 / ε ^ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * if ε ≤ z.2 ∧ z.2 ≤ 2 * ε then CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 else 0
The heat term in the Gaussian Carleman estimate is bounded by cutoff
energy and the two localized errors (eq:uc-cutoff-carleman).