Absorption in the Gaussian cutoff estimate #
The Carleman mass coefficient has a uniform positive lower bound when the normalized spatial radius is at least four.
theorem
ESS.uc_cutoff_carleman_energy_lower
{ρ ε : ℝ}
(hρ : 4 ≤ ρ)
(hε : 0 < ε)
{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 < ⊤)
:
have a := 1 / 100 * ρ ^ 2 / (2 * Real.log (CKN.gaussCarlemanTimeWeight (3 / 2)));
have Z := ucCutoffField (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v;
have DZ := ucCutoffDw (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv;
1 / 20 * ∫ (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 * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2 + ucGaussianWeight a z * CKN.spatialGradientSq Z DZ z
The positive Carleman field and gradient terms control one twentieth of the weighted cutoff energy on the normalized cylinder.