The half-space Carleman inequality

The componentwise conjugation and commutator identities for prop:carleman-halfspace.

@[instance_reducible]

def ESS.Main.instNormedAddCommGroupParabolicPoint : NormedAddCommGroup CKN.Foundation.Parabolic.ParabolicPoint

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

Equations

• ESS.Main.instNormedAddCommGroupParabolicPoint = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

noncomputable def ESS.Main.instNormedSpaceRealParabolicPoint : NormedSpace ℝ CKN.Foundation.Parabolic.ParabolicPoint

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

Equations

• ESS.Main.instNormedSpaceRealParabolicPoint = CKN.carlemanProductNormedSpace

theorem ESS.Main.testFunction_component {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hw : w ∈ CKN.spaceTimeTestFunction Ω I) (i : Fin 3) : (ContDiff ℝ ↑⊤ fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w z i) ∧ (HasCompactSupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w z i) ∧ (tsupport fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => w z i) ⊆ CKN.spaceTimeSet Ω I

A component of a smooth compactly supported space-time vector field has the same regularity and lies in the same support.

theorem ESS.Main.vec3EuclideanNorm_sq (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 = ∑ i : Fin 3, x i ^ 2

The Euclidean norm on three components squares to the coordinate sum.

theorem ESS.Main.spatialGradientSq_eq_sum_scalarGradSq (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialGradientSq w (CKN.spatialGradient w) z = ∑ i : Fin 3, CKN.scalarGradSq (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z

The vector spatial-gradient density is the sum of its scalar component densities.

theorem ESS.Main.heatVectorSq_eq_sum (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : (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 = ∑ i : Fin 3, (CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z + CKN.scalarLaplacian (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => w y i) z) ^ 2

The squared Euclidean norm of the componentwise heat operator is the sum of the scalar squares.

noncomputable def ESS.Main.halfSpaceMassFactor (α : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The mass weight x₃^{2α} t^{-α} of prop:carleman-halfspace.

Equations

• ESS.Main.halfSpaceMassFactor α z = z.1 2 ^ (2 * α) / z.2 ^ α

noncomputable def ESS.Main.halfSpaceNormalEnergy (a α : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The normal gradient energy t |∇φ⁽²⁾|² of prop:carleman-halfspace.

Equations

• ESS.Main.halfSpaceNormalEnergy a α z = z.2 * ESS.halfSpaceGradientTwo a α z ^ 2

theorem ESS.Main.halfSpace_estimate_of_pointwise_bound (hbound : ∀ (α : ℝ), 1 / 2 < α → α < 1 → ∀ (a : ℝ), 2 ≤ a → ∀ (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), ∀ z ∈ halfSpaceDomain, (a * (2 * α - 1) * halfSpaceMassFactor α z + halfSpaceNormalEnergy a α z) * v z ^ 2 ≤ CKN.carlemanCommutatorDensity (halfSpacePhase a α) v z) (α : ℝ) : 1 / 2 < α → α < 1 → ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (a : ℝ), a₀ < a → ∀ w ∈ 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 * (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * (1 - z.2) * z.1 2 ^ (2 * α) / z.2 ^ α)) * (a * CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 / z.2 ^ 2 + CKN.spatialGradientSq w (CKN.spatialGradient w) 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 * (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * (1 - z.2) * z.1 2 ^ (2 * α) / 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

The half-space Carleman estimate of prop:carleman-halfspace (with threshold two and constant 5 + 7/(2(2α − 1)) as witnesses), from the pointwise lower bound of the commutator density for halfSpacePhase.