Separating the lower-time error

The cutoff error consists of the error for the fixed spatial-phase cutoff, multiplied by a bounded time factor, and one term of size 8/ε.

noncomputable def ESS.buShortSpacePhaseGradientSize (scale R : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Sum of absolute spatial derivatives of the cutoff without its lower-time factor.

Equations

• ESS.buShortSpacePhaseGradientSize scale R hR z = ∑ j : Fin 3, |CKN.spatialPartial (ESS.buCutScalar (ESS.buShortSpacePhaseCutoff scale R hR)) j z|

noncomputable def ESS.buShortSpacePhaseHeatSize (scale R : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : ℝ

Absolute scalar heat derivative of the cutoff without its lower-time factor.

Equations

• One or more equations did not get rendered due to their size.

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

The two-factor cutoff takes values in the unit interval.

theorem ESS.buShortCutoffGradientSize_le_spacePhase (scale R ε : ℝ) (hR : 0 < R) (z : CKN.Foundation.Parabolic.ParabolicPoint) : buShortCutoffGradientSize scale R hR ε z ≤ buShortSpacePhaseGradientSize scale R hR z

Spatial derivative size of the full cutoff is bounded by that of the two-factor cutoff.