Smooth extension of the short-time phase

The phase can be smoothly clamped below the active normal and time ranges. This gives a globally smooth cutoff with the prescribed values on the half-space Carleman cylinder.

noncomputable def ESS.buShortClampedHeight (y : ℝ) : ℝ

A positive smooth extension of the normal height, equal to the height above two.

Equations

• ESS.buShortClampedHeight y = 1 + CKN.smoothTransitionProfile (y - 1) * (y - 1)

noncomputable def ESS.buShortClampedTime (s : ℝ) : ℝ

A positive smooth extension of the time, equal to the time from one half onward.

Equations

• ESS.buShortClampedTime s = 1 / 4 + CKN.smoothTransitionProfile (4 * s - 1) * (s - 1 / 4)

theorem ESS.buShortClampedHeight_pos (y : ℝ) : 0 < buShortClampedHeight y

The clamped normal height is positive everywhere.

theorem ESS.buShortClampedTime_pos (s : ℝ) : 0 < buShortClampedTime s

The clamped time is positive everywhere.

theorem ESS.buShortClampedHeight_eq {y : ℝ} (hy : 2 ≤ y) : buShortClampedHeight y = y

The clamped height agrees with height above two.

theorem ESS.buShortClampedTime_eq {s : ℝ} (hs : 1 / 2 ≤ s) : buShortClampedTime s = s

The clamped time agrees with time from one half onward.

theorem ESS.buShortClampedHeight_smooth : ContDiff ℝ (↑⊤) buShortClampedHeight

Both clamping functions are smooth.

theorem ESS.buShortClampedTime_smooth : ContDiff ℝ (↑⊤) buShortClampedTime

The time clamp is smooth.

noncomputable def ESS.buShortFExt (y s : ℝ) : ℝ

The globally smooth normal phase used to define the cutoff.

Equations

• ESS.buShortFExt y s = (1 - ESS.buShortClampedTime s) * ESS.buShortClampedHeight y ^ (3 / 2) * ESS.buShortClampedTime s ^ (-(3 / 4))

theorem ESS.buShortFExt_eq {y s : ℝ} (hy : 2 ≤ y) (hs : 1 / 2 ≤ s) : buShortFExt y s = buShortF y s

The extended phase agrees with the normal Carleman phase on the active height and time range.

theorem ESS.buShortFExt_smooth : ContDiff ℝ ↑⊤ fun (q : ℝ × ℝ) => buShortFExt q.1 q.2

The extended normal phase is smooth in both variables.

noncomputable def ESS.buShortEtaExt (scale : ℝ) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

A smooth extension of the normal-phase cutoff.

Equations

• ESS.buShortEtaExt scale q = ESS.buShortNormalCutoff scale (q.1 2) * ESS.buShortPhaseCutoff ((ESS.buShortFExt (q.1 2) q.2 - ESS.buShortB scale) / ESS.buShortB scale)

theorem ESS.buShortEtaExt_eq {scale : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) {q : CKN.Foundation.Parabolic.Vec3 × ℝ} (hy : buShortYMinus scale < q.1 2) (hs : 1 / 2 ≤ q.2) : buShortEtaExt scale q = buShortCutoff scale (q.1 2) q.2

The smooth extension agrees with the geometric cutoff in the active normal and time range.

theorem ESS.buShortEtaExt_eq_one_above_gap {scale : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) {q : CKN.Foundation.Parabolic.Vec3 × ℝ} (hy : 0 < q.1 2) (hs : 1 / 2 ≤ q.2) (hs1 : q.2 ≤ 1) (hphase : -buShortD scale / 2 < buShortF (q.1 2) q.2 - buShortB scale) : buShortEtaExt scale q = 1

The smooth extension equals one above the negative transition gap inside the active cylinder.

theorem ESS.buShortFExt_product_smooth : ContDiff ℝ ↑⊤ fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => buShortFExt (q.1 2) q.2

The extended phase is smooth in product space-time coordinates.

theorem ESS.buShortEtaExt_smooth (scale : ℝ) : ContDiff ℝ (↑⊤) (buShortEtaExt scale)

The extended normal-phase cutoff is smooth on the full product space.