Quantities for Gaussian unique continuation

The cylinder, Gaussian weight, and integral flatness condition are those of lem:uc-gaussian. The flatness predicate records the local all-orders integral assumption of that lemma.

def ESS.ucWeakHeatVector (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 weak heat operator formed from the specified second and time weak derivatives.

Equations

• ESS.ucWeakHeatVector D2w Dtw z i = Dtw z i + ∑ j : Fin 3, D2w z i j j

def ESS.UCIntegralFlatness (x₀ : CKN.Foundation.Parabolic.Vec3) (R T : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : Prop

Integral vanishing of every order at a boundary point (eq:uc-integral-vanishing).

Equations

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

noncomputable def ESS.ucLocalEnergy (x₀ : CKN.Foundation.Parabolic.Vec3) (R T : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : ℝ

The unweighted energy over the smaller cylinder used in the Gaussian box estimate (lem:uc-gaussian).

Equations

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

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

Gaussian weight in lem:uc-gaussian.

Equations

• ESS.ucGaussianWeight a z = CKN.gaussCarlemanTimeWeight z.2 ^ (-2 * a) * Real.exp (-CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2 / (4 * z.2))

def ESS.ucCylinder (ρ : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The scaled positive-time cylinder.

Equations

• ESS.ucCylinder ρ = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2)

def ESS.ucInnerRegion (ρ : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The plateau on which the spatial and time cutoffs equal one.

Equations

• ESS.ucInnerRegion ρ = CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 (ρ / 2)) (Set.Ioo 0 (3 / 2))

def ESS.ucCutoffRegion (ρ : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The region supporting derivatives of the spatial and final-time cutoffs.

Equations

• ESS.ucCutoffRegion ρ = ESS.ucCylinder ρ \ ESS.ucInnerRegion ρ

def ESS.ucScaledPoint (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.Foundation.Parabolic.ParabolicPoint

Parabolic translation and dilation about a boundary point.

Equations

• ESS.ucScaledPoint x₀ scale z = (x₀ + scale • z.1, scale ^ 2 * z.2)

def ESS.ucScaledField (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

A field viewed in translated parabolic coordinates.

Equations

• ESS.ucScaledField x₀ scale w z = w (ESS.ucScaledPoint x₀ scale z)

def ESS.ucScaledDw (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3

The first weak spatial derivative under parabolic dilation.

Equations

• ESS.ucScaledDw x₀ scale Dw z i j = scale * Dw (ESS.ucScaledPoint x₀ scale z) i j

def ESS.ucScaledD2w (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3

The second weak spatial derivative under parabolic dilation.

Equations

• ESS.ucScaledD2w x₀ scale D2w z i j k = scale ^ 2 * D2w (ESS.ucScaledPoint x₀ scale z) i j k

def ESS.ucScaledDtw (x₀ : CKN.Foundation.Parabolic.Vec3) (scale : ℝ) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The time weak derivative under parabolic dilation.

Equations

• ESS.ucScaledDtw x₀ scale Dtw z i = scale ^ 2 * Dtw (ESS.ucScaledPoint x₀ scale z) i