Bounds for the short-time cutoff

The three factors of the smooth cutoff lie between zero and one.

theorem ESS.buShortEtaExt_bounds (scale : ℝ) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ buShortEtaExt scale q ∧ buShortEtaExt scale q ≤ 1

The extended normal-phase cutoff takes values in the unit interval.

theorem ESS.buShortFullCutoff_bounds (scale R : ℝ) (hR : 0 < R) (ε : ℝ) (q : CKN.Foundation.Parabolic.Vec3 × ℝ) : 0 ≤ buShortFullCutoff scale R hR ε q ∧ buShortFullCutoff scale R hR ε q ≤ 1

The full compact cutoff takes values in the unit interval.

theorem ESS.buCut_spatialPartial_abs_le_sum (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) (j : Fin 3) : |CKN.spatialPartial (buCutScalar κ) j z| ≤ ∑ k : Fin 3, |CKN.spatialPartial (buCutScalar κ) k z|

The sum of the three absolute spatial derivatives is a pointwise bound for each individual derivative.