Conjugation of the backward heat operator

The pointwise change of variables used in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript and prop:carleman-halfspace of the Escauriaza–Seregin–Šverák manuscript.

@[instance_reducible]

def CKN.carlemanCoreConjugationNormedAddCommGroup : NormedAddCommGroup Foundation.Parabolic.ParabolicPoint

The product normed additive group structure used in the conjugation calculation.

Equations

• CKN.carlemanCoreConjugationNormedAddCommGroup = CKN.carlemanProductNormedAddCommGroup

@[instance_reducible]

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

The real product normed-space structure used in the conjugation calculation.

Equations

• CKN.carlemanCoreConjugationNormedSpace = CKN.carlemanProductNormedSpace

theorem CKN.carlemanConj_exp_mul {U : Set Foundation.Parabolic.ParabolicPoint} (hU : IsOpen U) {φ w : Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiffOn ℝ (↑⊤) φ U) (hw : ContDiff ℝ (↑⊤) w) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ U) : carlemanConj φ (fun (y : Foundation.Parabolic.ParabolicPoint) => Real.exp (φ y) * w y) z = Real.exp (φ z) * (timePartial w z + scalarLaplacian w z)

Exponential conjugation expands to the scalar backward heat operator on the open set where the phase is smooth.