Half-space Carleman phase bounds

The phase gradient and scalar commutator coefficients satisfy the bounds needed for the half-space Carleman inequality.

theorem ESS.halfSpacePhase_scalarGradSq (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) : CKN.scalarGradSq (halfSpacePhase a α) z = z.1 0 ^ 2 / (16 * z.2 ^ 2) + z.1 1 ^ 2 / (16 * z.2 ^ 2) + halfSpaceGradientTwo a α z ^ 2

The half-space phase has squared gradient equal to the sum of its tangential and normal contributions.

theorem ESS.halfSpacePhase_anisotropicFactor_ge_one (α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (hα : 0 < α) : 1 ≤ z.1 2 ^ (2 * α) / z.2 ^ α

The anisotropic spatial phase is at least one on the half-space slab.

theorem ESS.halfSpacePhase_timeGradient_bound (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (ha : 2 ≤ a) (hα : 0 < α) (hα1 : α ≤ 1) : z.2 * (2 * CKN.scalarGradSq (halfSpacePhase a α) z - CKN.timePartial (halfSpacePhase a α) z) ≤ 2 * z.2 * halfSpaceGradientTwo a α z ^ 2 + a * z.1 2 ^ (2 * α) / z.2 ^ α

The time derivative of the half-space phase gives the pointwise gradient estimate used in prop:carleman-halfspace.

theorem ESS.halfSpacePhase_commutatorDensity_expand (a α : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) : CKN.carlemanCommutatorDensity (halfSpacePhase a α) v z = z.2 * CKN.spatialPartial v 2 z ^ 2 + 4 * z.2 ^ 2 * CKN.spatialSecondPartial (halfSpacePhase a α) 2 2 z * CKN.spatialPartial v 2 z ^ 2 + z.2 ^ 2 * v z ^ 2 * (4 * CKN.spatialSecondPartial (halfSpacePhase a α) 2 2 z * halfSpaceGradientTwo a α z ^ 2 + -(CKN.spatialPartial (halfSpacePhase a α) 0 z ^ 2 + CKN.spatialPartial (halfSpacePhase a α) 1 z ^ 2) / z.2 + CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial (halfSpacePhase a α) y) z - 4 * ∑ i : Fin 3, CKN.spatialPartial (halfSpacePhase a α) i z * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (halfSpacePhase a α) i y) z - ∑ i : Fin 3, ∑ j : Fin 3, CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialSecondPartial (halfSpacePhase a α) i i y) j j z - CKN.scalarGradSq (halfSpacePhase a α) z / z.2 + CKN.timePartial (halfSpacePhase a α) z / z.2)

After cancellation of the two tangential coordinates, the half-space commutator density has only the normal derivative term and a scalar weight coefficient.

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

The zeroth-order scalar coefficient in the half-space commutator.

Equations

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

theorem ESS.halfSpacePhase_commutatorDensity_lower (a α : ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (ha : 2 ≤ a) (hαlo : 1 / 2 < α) (hαhi : α < 1) : a * (2 * α - 1) * z.1 2 ^ (2 * α) / z.2 ^ α * v z ^ 2 + z.2 * halfSpaceGradientTwo a α z ^ 2 * v z ^ 2 ≤ CKN.carlemanCommutatorDensity (halfSpacePhase a α) v z

The half-space Carleman commutator density has the pointwise lower bound used in prop:carleman-halfspace.

theorem ESS.halfSpaceAbsorption (P U V G D X a θ : ℝ) (hθ : 0 < θ) (ha : 2 ≤ a) (hV0 : 0 ≤ V) (hVU : V ≤ U) (hG0 : 0 ≤ G) (hMass : a * θ * U + G ≤ P) (hX : |X| ≤ √(V * P)) (hD : D ≤ |X| + 2 * G + a * U) : a * V + 2 * D ≤ (5 + 7 / (2 * θ)) * P

The real-variable absorption used at the end of prop:carleman-halfspace.