Derivatives of the normal phase

Explicit derivatives of the normal Carleman phase supply polynomial bounds for the smooth transition cutoff.

theorem ESS.buShortF_deriv_height {y s : ℝ} (hy : 0 < y) : deriv (fun (r : ℝ) => buShortF r s) y = 3 / 2 * (1 - s) * y ^ (1 / 2) * s ^ (-(3 / 4))

The first height derivative of the normal phase.

theorem ESS.buShortF_deriv_height_twice {y s : ℝ} (hy : 0 < y) : deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortF q s) r) y = 3 / 4 * (1 - s) * y ^ (-(1 / 2)) * s ^ (-(3 / 4))

The second height derivative of the normal phase.

theorem ESS.buShortF_deriv_time {y s : ℝ} (hs : 0 < s) : deriv (fun (t : ℝ) => buShortF y t) s = -(y ^ (3 / 2) * s ^ (-(3 / 4))) - 3 / 4 * (1 - s) * y ^ (3 / 2) * s ^ (-(7 / 4))

The time derivative of the normal phase.

theorem ESS.buShort_time_rpow_le_four {s p : ℝ} (hs : 1 / 2 ≤ s) (hs1 : s ≤ 1) (hp : -2 ≤ p) : s ^ p ≤ 4

On the active time interval, every power between s⁻² and one is bounded by four.

theorem ESS.buShort_height_rpow_le_sq {y p : ℝ} (hy : 1 ≤ y) (hp : p ≤ 2) : y ^ p ≤ y ^ 2

Any height power of exponent at most two is bounded by the square above height one.

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

The first height derivative has square-root height growth on the active half-space strip.

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

The second height derivative decays as the inverse square root of height on the active half-space strip.

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

The time derivative has three-halves power height growth on the active half-space strip.