Shell derivatives above the phase gap

On the normal-phase plateau only the spatial ball cutoff contributes to the spatial and heat derivative sizes.

theorem ESS.buShortSpacePhaseGradientSize_shell_on_aboveGap {scale R : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale) : buShortSpacePhaseGradientSize scale R hR z ≤ 3 * (CKN.cutoffGradientConstant / (2 * R))

Above the negative phase gap, the gradient size is bounded by the spatial shell derivative.

theorem ESS.buShortSpacePhaseHeatSize_shell_on_aboveGap {scale R : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale) : buShortSpacePhaseHeatSize scale R hR z ≤ 3 * (CKN.cutoffSecondDerivativeConstant / (2 * R) ^ 2)

Above the negative phase gap, the scalar heat size is bounded by the spatial shell second derivatives.