The conjugated heat operator and its commutator density

Scalar forms of the quantities used in the proofs of prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript and prop:carleman-halfspace of the same manuscript. For a weight φ and a scalar field v, carlemanConj φ v is e^φ L (e^{-φ} v) with L = ∂ₜ + Δ, written as ∂ₜv + Δv - 2∇φ·∇v + (|∇φ|² - ∂ₜφ - Δφ) v, and carlemanCommutatorDensity φ v is the integrand of the commutator identity eq:carleman-commutator of the Escauriaza–Seregin–Šverák manuscript: `4t²(φ_{ij} ∂ᵢv ∂ⱼv + φ_{ij} φᵢ φⱼ v²)

• t² v² (∂ₜ²φ - 2∂ₜ|∇φ|² - Δ²φ) + t|∇v|² - t v² (|∇φ|² - ∂ₜφ). Here ∂ₜ|∇φ|²is written as2 ∑ᵢ φᵢ ∂ₜφᵢ`.

noncomputable def CKN.scalarGradSq (f : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The squared spatial gradient |∇f|² of a scalar field.

Equations

• CKN.scalarGradSq f z = ∑ i : Fin 3, CKN.spatialPartial f i z ^ 2

noncomputable def CKN.scalarLaplacian (f : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The spatial Laplacian Δf of a scalar field.

Equations

• CKN.scalarLaplacian f z = ∑ i : Fin 3, CKN.spatialSecondPartial f i i z

noncomputable def CKN.carlemanConj (φ v : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The conjugated heat operator e^φ (∂ₜ + Δ)(e^{-φ} v) in expanded form.

Equations

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

noncomputable def CKN.carlemanCommutatorDensity (φ v : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) : ℝ

The integrand of the commutator identity eq:carleman-commutator (ESS).

Equations

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