Absorbed Gaussian cutoff estimate #
The universal Gaussian Carleman constant and a sufficiently small parabolic scale absorb the weak heat lower order term.
theorem
ESS.uc_cutoff_energy_absorbed :
∃ (c₀ : ℝ),
0 < c₀ ∧ ∀ (ρ ε c₁ scale : ℝ) (hρ : 4 ≤ ρ),
0 < ε →
0 ≤ c₁ →
0 ≤ scale →
c₀ * 54 * (c₁ * scale) ^ 2 ≤ 1 / 40 →
∀ (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),
CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dv D2v Dtv →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤ →
(∀ᵐ (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;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2 + CKN.spatialGradientSq Z DZ z) ≤ 40 * c₀ * ((∫ (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)
There is one Gaussian constant for which every normalized cutoff obeys the absorbed estimate when the lower order scale is small.