Separating the lower-time cutoff

The lower-time factor has no spatial derivatives. These identities isolate its one derivative from the fixed spatial and phase factors.

noncomputable def ESS.buShortSpacePhaseCutoff (scale R : ℝ) (hR : 0 < R) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : ℝ

The product of the spatial and normal-phase cutoff factors.

Equations

• ESS.buShortSpacePhaseCutoff scale R hR q = ESS.ucSpatialCutoff (2 * R) ⋯ q.1 * ESS.buShortEtaExt scale q

theorem ESS.buShortSpacePhaseCutoff_smooth (scale R : ℝ) (hR : 0 < R) : ContDiff ℝ (↑⊤) (buShortSpacePhaseCutoff scale R hR)

The two-factor cutoff is smooth.

theorem ESS.buShortFullCutoff_spatialPartial_time_factor (scale R ε : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) : CKN.spatialPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j z = CKN.spatialPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) j z * buShortTimeCutoff ε z.2

The spatial first derivative carries the lower-time factor without differentiating it.

theorem ESS.buShortFullCutoff_spatialSecondPartial_time_factor (scale R ε : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : CKN.spatialSecondPartial (buCutScalar (buShortFullCutoff scale R hR ε)) i j z = CKN.spatialSecondPartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) i j z * buShortTimeCutoff ε z.2

The spatial second derivative also carries the lower-time factor without differentiating it.

theorem ESS.buShortFullCutoff_timePartial_time_factor (scale R ε : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (buCutScalar (buShortFullCutoff scale R hR ε)) z = CKN.timePartial (buCutScalar (buShortSpacePhaseCutoff scale R hR)) z * buShortTimeCutoff ε z.2 + buShortSpacePhaseCutoff scale R hR (z.1, z.2) * deriv (buShortTimeCutoff ε) z.2

The only lower-time derivative appears in the time product rule.