Compact cutoffs for the short-time Carleman estimate

A ball cutoff, the normal-phase cutoff, and a lower-time cutoff are multiplied before applying the weak half-space estimate.

noncomputable def ESS.buShortTimeCutoff (ε s : ℝ) : ℝ

The lower-time cutoff, starting at time one half plus ε.

Equations

• ESS.buShortTimeCutoff ε s = ESS.ucInitialTimeCutoff ε (s - 1 / 2)

noncomputable def ESS.buShortFullCutoff (scale R : ℝ) (hR : 0 < R) (ε : ℝ) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The full scalar cutoff on product coordinates.

Equations

• ESS.buShortFullCutoff scale R hR ε q = ESS.ucSpatialCutoff (2 * R) ⋯ q.1 * ESS.buShortEtaExt scale q * ESS.buShortTimeCutoff ε q.2

theorem ESS.buShortTimeCutoff_smooth (ε : ℝ) : ContDiff ℝ (↑⊤) (buShortTimeCutoff ε)

The lower-time cutoff is smooth for every fixed ε.

theorem ESS.buShortFullCutoff_smooth (scale R : ℝ) (hR : 0 < R) (ε : ℝ) : ContDiff ℝ (↑⊤) (buShortFullCutoff scale R hR ε)

The full scalar cutoff is globally smooth.