Carleman Half Weights Derivatives

Weight bounds used in the half-space Carleman estimate.

@[instance_reducible]

def ESS.halfWeightsTopologicalSpace : TopologicalSpace CKN.Foundation.Parabolic.ParabolicPoint

The product topology used to differentiate the half-space Carleman weights.

Equations

• ESS.halfWeightsTopologicalSpace = instTopologicalSpaceProd

@[instance_reducible]

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

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

Equations

• ESS.halfWeightsNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• ESS.halfWeightsNormedSpace = CKN.carlemanProductNormedSpace

def ESS.halfSpaceDomain : Set CKN.Foundation.Parabolic.ParabolicPoint

The open half-space and time slab used by prop:carleman-halfspace.

Equations

• ESS.halfSpaceDomain = {x : CKN.Foundation.Parabolic.Vec3 | 1 < x 2} ×ˢ Set.Ioo 0 1

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

The anisotropic phase in prop:carleman-halfspace.

Equations

• ESS.halfSpacePhase a α z = -(z.1 0 ^ 2 + z.1 1 ^ 2) / (8 * z.2) + a * (1 - z.2) * z.1 2 ^ (2 * α) / z.2 ^ α

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

The normal component of the spatial gradient of the half-space phase.

Equations

• ESS.halfSpaceGradientTwo a α z = 2 * α * a * (1 - z.2) * z.1 2 ^ (2 * α - 1) / z.2 ^ α

theorem ESS.isOpen_halfSpaceDomain : IsOpen halfSpaceDomain

The half-space in space times the time interval (0,1) is open.

theorem ESS.halfSpacePhase_contDiffOn (a α : ℝ) : ContDiffOn ℝ (↑⊤) (halfSpacePhase a α) halfSpaceDomain

The half-space phase is smooth on its domain.

theorem ESS.halfSpacePhase_spatialPartial (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (i : Fin 3) : CKN.spatialPartial (halfSpacePhase a α) i z = if i = 2 then halfSpaceGradientTwo a α z else -z.1 i / (4 * z.2)

The explicit spatial gradient of the half-space phase on its domain.

theorem ESS.halfSpacePhase_spatialSecondPartial (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (i j : Fin 3) : CKN.spatialSecondPartial (halfSpacePhase a α) i j z = if i = j then if i = 2 then 2 * α * (2 * α - 1) * a * (1 - z.2) * z.1 2 ^ (2 * α - 2) / z.2 ^ α else -(1 / (4 * z.2)) else 0

The explicit spatial Hessian of the half-space phase on its domain.

theorem ESS.halfSpacePhase_spatialFourthDiagonal (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (i j : Fin 3) : CKN.spatialSecondPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialSecondPartial (halfSpacePhase a α) i i y) j j z = if i = 2 ∧ j = 2 then 2 * α * (2 * α - 1) * (2 * α - 2) * (2 * α - 3) * a * (1 - z.2) * z.1 2 ^ (2 * α - 4) / z.2 ^ α else 0

The explicit fourth spatial derivative of the diagonal Hessian entries.

theorem ESS.halfSpacePhase_timePartial (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) : CKN.timePartial (halfSpacePhase a α) z = (z.1 0 ^ 2 + z.1 1 ^ 2) / 8 * z.2 ^ (-2) - a * z.1 2 ^ (2 * α) * z.2 ^ (-α - 1) * (α + (1 - α) * z.2)

The first time derivative of the half-space phase on its domain.

theorem ESS.halfSpacePhase_timeSecondPartial (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial (halfSpacePhase a α) y) z = -((z.1 0 ^ 2 + z.1 1 ^ 2) / 4) * z.2 ^ (-3) + a * z.1 2 ^ (2 * α) * z.2 ^ (-α - 2) * (α * (α + 1) + α * (1 - α) * z.2)

The second time derivative of the half-space phase on its domain.

theorem ESS.halfSpacePhase_timeSpatialPartial (a α : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ halfSpaceDomain) (i : Fin 3) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (halfSpacePhase a α) i y) z = if i = 2 then -2 * α * a * z.1 2 ^ (2 * α - 1) * z.2 ^ (-α - 1) * (α + (1 - α) * z.2) else z.1 i / 4 * z.2 ^ (-2)

The time derivative of every spatial component of the half-space gradient.