Derivatives of the Gaussian Carleman phase

The calculations below specialize eq:carleman-commutator of the Escauriaza–Seregin–Šverák manuscript to the phase in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript.

@[instance_reducible]

def CKN.gaussDerivativesNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure on space-time for Gaussian derivative calculations.

Equations

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

@[instance_reducible]

noncomputable def CKN.gaussDerivativesNormedSpace : NormedSpace ℝ Foundation.Parabolic.ParabolicPoint

The real product normed-space structure on space-time for Gaussian derivative calculations.

Equations

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

theorem CKN.gaussCarlemanPhase_spatialSecondPartial (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) (i j : Fin 3) : spatialSecondPartial (gaussCarlemanPhase q) i j z = if i = j then -1 / (4 * z.2) else 0

The spatial Hessian of the Gaussian phase on positive time.

theorem CKN.gaussCarlemanPhase_scalarGradSq (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : scalarGradSq (gaussCarlemanPhase q) z = (∑ i : Fin 3, z.1 i ^ 2) / (16 * z.2 ^ 2)

The squared spatial gradient of the Gaussian phase.

theorem CKN.gaussCarlemanPhase_potential (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : scalarGradSq (gaussCarlemanPhase q) z - timePartial (gaussCarlemanPhase q) z = -scalarGradSq (gaussCarlemanPhase q) z + q * (1 / z.2 - 1 / 3)

The phase potential in the conjugated heat operator.

theorem CKN.gaussCarlemanPhase_scalarLaplacian (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : scalarLaplacian (gaussCarlemanPhase q) z = -3 / (4 * z.2)

The spatial Laplacian of the Gaussian phase.

theorem CKN.gaussCarlemanPhase_time_spatialPartial (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) (i : Fin 3) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (gaussCarlemanPhase q) i y) z = z.1 i / (4 * z.2 ^ 2)

The time derivative of each spatial derivative of the Gaussian phase.

theorem CKN.gaussCarlemanPhase_time_timePartial (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => timePartial (gaussCarlemanPhase q) y) z = (-∑ i : Fin 3, z.1 i ^ 2) / (4 * z.2 ^ 3) + q / z.2 ^ 2

The second time derivative of the Gaussian phase.

theorem CKN.gaussCarlemanPhase_spatial_third (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) (i j k : Fin 3) : spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialSecondPartial (gaussCarlemanPhase q) i j y) k z = 0

Every third spatial derivative of the Gaussian phase vanishes.

theorem CKN.gaussCarlemanPhase_spatial_fourth (q : ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) (i j : Fin 3) : spatialSecondPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialSecondPartial (gaussCarlemanPhase q) i i y) j j z = 0

Every fourth spatial derivative entering Δ²φ vanishes.

theorem CKN.gaussCarleman_commutatorDensity (q : ℝ) (v : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) (ht : 0 < z.2) : carlemanCommutatorDensity (gaussCarlemanPhase q) v z = q / 3 * z.2 * v z ^ 2

The commutator density for the Gaussian phase is positive and explicit.

theorem CKN.gaussCarlemanPhase_contDiffOn (q : ℝ) : ContDiffOn ℝ (↑⊤) (gaussCarlemanPhase q) (spaceTimeSet Set.univ (Set.Ioo 0 2))

The Gaussian phase is smooth on the positive-time cylinder.