Uniform polynomial bounds for cutoff derivative sizes

For radii at least one, the derivative sizes are controlled by fixed coefficients times the square of one plus the normal height.

noncomputable def ESS.buShortUniformGradientCoeff (scale : ℝ) : ℝ

A radius-independent coefficient for the sum of spatial cutoff derivatives.

Equations

• ESS.buShortUniformGradientCoeff scale = 3 * (CKN.cutoffGradientConstant + 16 + 48 * (12 / ESS.buShortB scale))

noncomputable def ESS.buShortUniformHeatCoeff (scale C₁ C₂ : ℝ) : ℝ

A radius-independent coefficient for the scalar heat derivative.

Equations

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

theorem ESS.buShortSpacePhaseGradientSize_uniform {scale R : ℝ} (hscale : 0 < scale) (hR : 1 ≤ R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hy : 2 < z.1 2) (hs : 1 / 2 ≤ z.2) (hs1 : z.2 ≤ 1) : buShortSpacePhaseGradientSize scale R ⋯ z ≤ buShortUniformGradientCoeff scale * (1 + z.1 2) ^ 2

The gradient size of the spatial-phase cutoff has a quadratic height bound uniform over spatial radii at least one.

theorem ESS.buShortSpacePhaseHeatSize_uniform {scale R C₁ C₂ : ℝ} (hscale : 0 < scale) (hR : 1 ≤ R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (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₂) : buShortSpacePhaseHeatSize scale R ⋯ z ≤ buShortUniformHeatCoeff scale C₁ C₂ * (1 + z.1 2) ^ 2

The scalar heat size of the spatial-phase cutoff has a quadratic height bound uniform over spatial radii at least one.