Carleman estimate for a compact Gaussian cutoff #
The weak product identities make the cut off field admissible for the Gaussian Carleman inequality.
theorem
ESS.uc_gaussian_cutoff_carleman_with_constant
(c₀ : ℝ)
(hgaussRaw :
∀ (a : ℝ),
0 < a →
∀ v ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 2),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), (z.2 * Real.exp ((1 - z.2) / 3)) ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v (CKN.spatialGradient v) z) ≤ c₀ * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), (z.2 * Real.exp ((1 - z.2) / 3)) ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) =>
CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) z + ∑ j : Fin 3,
CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => v y i) j j z) ^ 2)
{ρ ε : ℝ}
(hρ : 0 < ρ)
(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 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;
∀ (a : ℝ),
0 < a →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2, ucGaussianWeight a z * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2 + ucGaussianWeight a z * ∑ i : Fin 3, ∑ j : Fin 3, DZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j ^ 2 ≤ c₀ * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2, ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (LZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2
A fixed Gaussian Carleman constant applies to the compact cutoff of a normalized weak field.
theorem
ESS.uc_gaussian_cutoff_carleman
{ρ ε : ℝ}
(hρ : 0 < ρ)
(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 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;
∃ (c₀ : ℝ),
0 < c₀ ∧ ∀ (a : ℝ),
0 < a →
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2, ucGaussianWeight a z * (a / z.2) * CKN.Foundation.Parabolic.vec3EuclideanNorm (Z (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2 + ucGaussianWeight a z * ∑ i : Fin 3, ∑ j : Fin 3, DZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) i j ^ 2 ≤ c₀ * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ioo 0 2, ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (LZ (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z)) ^ 2
The Gaussian Carleman estimate applies to the compact cutoff of a normalized weak field.