Derivatives of the spatial and normal cutoffs

The two-factor cutoff separates the normal-phase derivatives from the spatial shell derivatives.

theorem ESS.buShortSpacePhase_spatialPartial (scale R : ℝ) (hR : 0 < R) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) j z = CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff (2 * R) ⋯ q.1) j z * buShortEtaExt scale (z.1, z.2) + ucSpatialCutoff (2 * R) ⋯ z.1 * CKN.spatialPartial (buCutScalar (buShortEtaExt scale)) j z

First spatial product rule for the two-factor cutoff.

theorem ESS.buShortSpacePhase_spatialSecondPartial_diag (scale R : ℝ) (hR : 0 < R) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialSecondPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) j j z = CKN.spatialSecondPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff (2 * R) ⋯ q.1) j j z * buShortEtaExt scale (z.1, z.2) + 2 * CKN.spatialPartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff (2 * R) ⋯ q.1) j z * CKN.spatialPartial (buCutScalar (buShortEtaExt scale)) j z + ucSpatialCutoff (2 * R) ⋯ z.1 * CKN.spatialSecondPartial (buCutScalar (buShortEtaExt scale)) j j z

Diagonal spatial second product rule for the two-factor cutoff.

theorem ESS.buShortSpatialCutoff_timePartial_zero (R : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ucSpatialCutoff (2 * R) ⋯ q.1) z = 0

The spatial cutoff has zero time derivative.

theorem ESS.buShortSpacePhase_timePartial (scale R : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) z = ucSpatialCutoff (2 * R) ⋯ z.1 * CKN.timePartial (buCutScalar (buShortEtaExt scale)) z

The time derivative of the two-factor cutoff comes entirely from the normal-phase factor.