Closed normal edge of the negative phase gap

Including the closed lower edge of the normal transition lets every nonzero cutoff error be assigned to the negative phase region or the spatial shell.

def ESS.buShortWideGapRegion (scale : ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The negative phase region including the lower normal transition edge.

Equations

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

theorem ESS.buShortWideGapRegion_measurable (scale : ℝ) : MeasurableSet (buShortWideGapRegion scale)

The region containing all normal-phase derivative errors is measurable.

theorem ESS.buShortShiftedWeight_le_on_wideGap {scale a : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (ha : 0 ≤ a) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ buShortWideGapRegion scale) : buShortShiftedWeight scale a z ≤ Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * Real.exp (-(a * buShortD scale))

The shifted weight gains the fixed negative phase factor on the wide gap region.

theorem ESS.buShortCutoffHeatErrorSize_aboveGap_of_not_wideGap {scale R ε c₁ : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hs : 1 / 2 < z.2) (hs1 : z.2 < 1) (hz : buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ≠ 0) (hnot : z ∉ buShortWideGapRegion scale) : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale

Any nonzero cutoff error above the negative phase gap lies on the open plateau of the normal cutoff.