Cutoff data for Gaussian unique continuation

The first and second weak derivative fields of a cut off vector field are written component first and spatial derivative indices afterward.

def ESS.ucCutoffScalar (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

The product of spatial, final-time, and initial-time cutoffs.

Equations

• ESS.ucCutoffScalar θ η χ z = θ z.1 * η z.2 * χ z.2

def ESS.ucCutoffField (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The cut off vector field of lem:uc-gaussian.

Equations

• ESS.ucCutoffField θ η χ v z = ESS.ucCutoffScalar θ η χ z • v z

noncomputable def ESS.ucCutoffDw (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Fin 3 → CKN.Foundation.Parabolic.Vec3

The first spatial derivative data of a cut off field.

Equations

• ESS.ucCutoffDw θ η χ v Dw z i j = ESS.ucCutoffScalar θ η χ z * Dw z i j + v z i * CKN.spatialPartial (ESS.ucCutoffScalar θ η χ) j z

noncomputable def ESS.ucCutoffD2 (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3

The second spatial derivative data of a cut off field.

Equations

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

noncomputable def ESS.ucCutoffDt (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

The time derivative data of a cut off field.

Equations

• ESS.ucCutoffDt θ η χ v Dtw z i = ESS.ucCutoffScalar θ η χ z * Dtw z i + v z i * CKN.timePartial (ESS.ucCutoffScalar θ η χ) z

noncomputable def ESS.ucCutoffHeat (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.Vec3

The heat operator acting on the cut off field, expressed through the specified weak derivative data.

Equations

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

theorem ESS.ucCutoffHeat_eq_weakHeat (θ : CKN.Foundation.Parabolic.Vec3 → ℝ) (η χ : ℝ → ℝ) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ucCutoffHeat θ η χ v Dw D2w Dtw z = ucWeakHeatVector (ucCutoffD2 θ η χ v Dw D2w) (ucCutoffDt θ η χ v Dtw) z

The product expansion agrees componentwise with the weak heat operator.