Integrable Gaussian cutoff terms #
The Carleman field, gradient, and heat terms are integrable in product coordinates for every positive initial cutoff time.
theorem
ESS.uc_weighted_cutoff_components_integrable
{ρ ε a : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(ha : 0 ≤ a)
{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 Z := ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v;
have DZ := ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv;
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2)
(ucCylinder ρ) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucGaussianWeight a z * CKN.spatialGradientSq Z DZ z)
(ucCylinder ρ) MeasureTheory.volume
The field and gradient parts of the weighted cutoff energy are individually integrable.
theorem
ESS.uc_weighted_cutoff_mass_over_time_integrable
{ρ ε a : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(ha : 0 ≤ a)
{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 Z := ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v;
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
ucGaussianWeight a z * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2)
(ucCylinder ρ) MeasureTheory.volume
The positive-time cutoff makes the Carleman mass term integrable, including its inverse time factor.
theorem
ESS.uc_cutoff_carleman_integrable_product
{ρ ε a : ℝ}
(hρ : 0 < ρ)
(hε : 0 < ε)
(ha : 0 ≤ a)
{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 Z := ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v;
have DZ := ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv;
have LZ := ucCutoffHeat (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv D2v Dtv;
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
ucGaussianWeight a (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2 + ucGaussianWeight a (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) * ∑ i : Fin 3, ∑ j : Fin 3, DZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j ^ 2)
(CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
ucGaussianWeight a (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) * CKN.Foundation.Parabolic.vec3EuclideanNorm (LZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2)
(CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2) MeasureTheory.volume
Both sides of the Gaussian cutoff Carleman inequality are integrable in product coordinates at positive initial cutoff time.