Space-time derivatives of the normal cutoff

The factor-wise derivatives of the normal cutoff reduce to its one-dimensional height and time derivatives.

theorem ESS.buShortEtaExt_spatialPartial (scale : ℝ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (buCutScalar (buShortEtaExt scale)) j z = deriv (fun (y : ℝ) => buShortEtaScalar scale y z.2) (z.1 2) * if j = 2 then 1 else 0

Only the normal coordinate contributes to the spatial gradient of the normal cutoff.

theorem ESS.buShortEtaExt_spatialSecondPartial_diag {scale : ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (j : Fin 3) : CKN.spatialSecondPartial (buCutScalar (buShortEtaExt scale)) j j z = if j = 2 then deriv (fun (y : ℝ) => deriv (fun (r : ℝ) => buShortEtaScalar scale r z.2) y) (z.1 2) else 0

Only the normal coordinate contributes to the diagonal Hessian of the normal cutoff.

theorem ESS.buShortEtaExt_timePartial (scale : ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (buCutScalar (buShortEtaExt scale)) z = deriv (fun (s : ℝ) => buShortEtaScalar scale (z.1 2) s) z.2

The time partial derivative of the normal cutoff is its scalar time derivative.

theorem ESS.buShortEtaExt_spatialPartial_bound {scale : ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hscale : 0 < scale) (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (hs1 : z.2 ≤ 1) (j : Fin 3) : |CKN.spatialPartial (buCutScalar (buShortEtaExt scale)) j z| ≤ (16 + 48 * (12 / buShortB scale)) * (1 + z.1 2)

Each spatial derivative of the normal cutoff has linear height growth on the active strip.

theorem ESS.buShortEtaExt_spatialSecondPartial_diag_bound {scale C₁ C₂ : ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hscale : 0 < scale) (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (hs1 : z.2 ≤ 1) (hC₁ : 0 ≤ C₁) (hN : ∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) (hC₂ : 0 ≤ C₂) (hP : ∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) (j : Fin 3) : |CKN.spatialSecondPartial (buCutScalar (buShortEtaExt scale)) j j z| ≤ (C₁ + 1536 * (12 / buShortB scale) + 36 * C₂ * (12 / buShortB scale) ^ 2 + 24 * (12 / buShortB scale)) * (1 + z.1 2) ^ 2

Each diagonal spatial second derivative of the normal cutoff has quadratic height growth on the active strip.

theorem ESS.buShortEtaExt_timePartial_bound {scale : ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hscale : 0 < scale) (hy : 2 < z.1 2) (hs : 1 / 2 < z.2) (hs1 : z.2 ≤ 1) : |CKN.timePartial (buCutScalar (buShortEtaExt scale)) z| ≤ 56 * (12 / buShortB scale) * (1 + z.1 2) ^ 2

The time partial derivative of the normal cutoff has quadratic height growth on the active strip.