Derivatives of the normal cutoff

The two-variable scalar cutoff is a product of a fixed-width height transition and the smooth normal-phase transition.

noncomputable def ESS.buShortEtaScalar (scale y s : ℝ) : ℝ

The scalar form of the extended normal cutoff.

Equations

• ESS.buShortEtaScalar scale y s = ESS.buShortNormalCutoff scale y * ESS.buShortPhaseFactor scale y s

theorem ESS.buShortEtaScalar_height_differentiable (scale s : ℝ) : Differentiable ℝ fun (y : ℝ) => buShortEtaScalar scale y s

The normal cutoff is differentiable in height at every point.

theorem ESS.buShortEtaScalar_deriv_height (scale y s : ℝ) : deriv (fun (r : ℝ) => buShortEtaScalar scale r s) y = deriv (buShortNormalCutoff scale) y * buShortPhaseFactor scale y s + buShortNormalCutoff scale y * deriv (fun (r : ℝ) => buShortPhaseFactor scale r s) y

The first height derivative obeys the product rule.

theorem ESS.buShortEtaScalar_height_deriv_differentiable {scale y s : ℝ} (hy : 2 < y) (hs : 1 / 2 ≤ s) : DifferentiableAt ℝ (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortEtaScalar scale q s) r) y

The first height derivative of the normal cutoff is differentiable on the active strip.

theorem ESS.buShortEtaScalar_deriv_time (scale y s : ℝ) : deriv (fun (t : ℝ) => buShortEtaScalar scale y t) s = buShortNormalCutoff scale y * deriv (fun (t : ℝ) => buShortPhaseFactor scale y t) s

The time derivative acts only on the phase transition factor.

theorem ESS.buShortEtaScalar_deriv_height_twice (scale y s : ℝ) (hy : 2 < y) (hs : 1 / 2 ≤ s) : deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortEtaScalar scale q s) r) y = deriv (deriv (buShortNormalCutoff scale)) y * buShortPhaseFactor scale y s + 2 * deriv (buShortNormalCutoff scale) y * deriv (fun (r : ℝ) => buShortPhaseFactor scale r s) y + buShortNormalCutoff scale y * deriv (fun (r : ℝ) => deriv (fun (q : ℝ) => buShortPhaseFactor scale q s) r) y

The second height derivative obeys the iterated product rule.