Gaussian and half-space Sobolev Carleman estimates

The Gaussian smooth estimate is supplied by prop:carleman-gauss; the half-space estimate is left as a smooth hypothesis so it can be connected to prop:carleman-halfspace.

noncomputable def ESS.gaussianDensity (a : ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The Gaussian Carleman density at parameter a and space-time point z.

Equations

• ESS.gaussianDensity a z = CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2))

noncomputable def ESS.gaussianMassWeight (a : ℝ) (z : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The Gaussian density multiplied by the time mass factor a / z.2.

Equations

• ESS.gaussianMassWeight a z = ESS.gaussianDensity a z * (a / z.2)

@[instance_reducible]

noncomputable def ESS.gaussianMeasureSpace : MeasureTheory.MeasureSpace CKN.Foundation.Parabolic.ParabolicPoint

The explicit Gaussian measure-space structure used for parabolic integral conversion.

Equations

• ESS.gaussianMeasureSpace = ESS.gaussExplicitMeasureSpace

theorem ESS.bu_carleman_sobolev_gaussian (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hderiv : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo 0 2) w Dw D2w Dtw) (hcompact : HasCompactSupport w) (htsupport : tsupport w ⊆ CKN.spaceTimeSet Set.univ (Set.Ioo 0 2)) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (a : ℝ) : 0 < a → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (a / z.2 * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 + CKN.spatialGradientSq w Dw z) ≤ Real.exp (4 / 3) * (9 + 2 * √6) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 2), CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2)) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ^ 2

The Gaussian Carleman inequality with its explicit constant extends to compactly supported space-time weak fields (lem:carleman-sobolev).

theorem ESS.bu_carleman_sobolev_halfspace (α : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hderiv : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hcompact : HasCompactSupport w) (htsupport : tsupport w ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1)) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hSmooth : ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (a : ℝ), a₀ < a → ∀ v ∈ CKN.spaceTimeTestFunction {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * halfSpacePhase a α z) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq v (CKN.spatialGradient v) z / z.2) ≤ c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * halfSpacePhase a α z) * (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) : ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (a : ℝ), a₀ < a → ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * halfSpacePhase a α z) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq w Dw z / z.2) ≤ c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} (Set.Ioo 0 1), z.2 ^ 2 * Real.exp (2 * halfSpacePhase a α z) * (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ^ 2

The half-space density passage preserves any smooth weighted Carleman estimate supplied for the stated domain (lem:carleman-sobolev).