The Gaussian Carleman estimate with its explicit constant

The shared commutator estimate, Gaussian weight identities, and componentwise energy bounds give prop:carleman-gauss with the constant c₀ = e^{4/3}(9 + 2√6).

@[instance_reducible]

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

Product Lebesgue measure on parabolic space-time.

Equations

• ESS.gaussExplicitMeasureSpace = MeasureTheory.Measure.prod.measureSpace

@[instance_reducible]

def ESS.gaussExplicitNormedAddCommGroup : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

The product norm on parabolic space-time used for classical differentiation.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable def ESS.gaussExplicitNormedSpace : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

The real scalar action compatible with the product norm on parabolic space-time.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.carlemanGaussian_explicit (a : ℝ) (ha : 0 < a) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hwtest : w ∈ 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 (w z) ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) z) ≤ Real.exp (4 / 3) * (9 + 2 * √6) * ∫ (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) => w y i) z + ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) j j z) ^ 2

Gaussian Carleman inequality on the positive-time cylinder with the explicit constant c₀ = e^{4/3}(9 + 2√6) (prop:carleman-gauss).