Derivatives of the extended normal phase

On the active region, the smooth global phase extension has the same derivatives as the normal Carleman phase.

theorem ESS.buShortFExt_deriv_height_eq {y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) : deriv (fun (r : ℝ) => buShortFExt r s) y = deriv (fun (r : ℝ) => buShortF r s) y

The first height derivative of the smooth extension agrees with the normal phase above height two.

theorem ESS.buShortFExt_deriv_height_twice_eq {y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) : deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortFExt q s) r) y = deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortF q s) r) y

The second height derivative of the smooth extension agrees with that of the normal phase above height two.

theorem ESS.buShortFExt_deriv_time_eq {y s : ℝ} (hy : 2 ≤ y) (hs : 1 / 2 < s) : deriv (fun (t : ℝ) => buShortFExt y t) s = deriv (fun (t : ℝ) => buShortF y t) s

The time derivative of the smooth extension agrees with the normal phase after time one half.

theorem ESS.buShortFExt_deriv_height_bound {y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) : |deriv (fun (r : ℝ) => buShortFExt r s) y| ≤ 6 * y ^ (1 / 2)

The first height derivative of the smooth phase has square-root height growth on the active region.

theorem ESS.buShortFExt_deriv_height_twice_bound {y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) : |deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortFExt q s) r) y| ≤ 3 * y ^ (-(1 / 2))

The second height derivative of the smooth phase decays as the inverse square root of height.

theorem ESS.buShortFExt_deriv_time_bound {y s : ℝ} (hy : 2 ≤ y) (hs : 1 / 2 < s) (hs1 : s ≤ 1) : |deriv (fun (t : ℝ) => buShortFExt y t) s| ≤ 7 * y ^ (3 / 2)

The time derivative of the smooth phase has three-halves power height growth on the active region.