Lower normal height of the compact cutoff support

The compact cutoff support remains above the closed lower edge of its normal transition.

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

The high normal strip containing all compact short-time cutoffs.

Equations

• ESS.buShortHighStrip scale = {z : CKN.Foundation.Parabolic.ParabolicPoint | ESS.buShortYMinus scale ≤ z.1 2 ∧ 1 / 2 < z.2 ∧ z.2 < 1}

theorem ESS.buShortCutSupport_height_lower (scale R ε : ℝ) (hR : 0 < R) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ buCutSupportSet (buShortFullCutoff scale R hR ε)) : buShortYMinus scale ≤ z.1 2

Every point of the compact cutoff support is at or above the lower normal transition height.

theorem ESS.buShortCutSupport_subset_highStrip (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : buCutSupportSet (buShortFullCutoff scale R hR ε) ⊆ buShortHighStrip scale

The support of every compact short-time cutoff lies in the high normal strip.

theorem ESS.buShortHighStrip_measurable (scale : ℝ) : MeasurableSet (buShortHighStrip scale)

The high normal strip is measurable.

theorem ESS.buShortWideGapRegion_subset_highStrip (scale : ℝ) : buShortWideGapRegion scale ⊆ buShortHighStrip scale

The negative phase gap is contained in the high normal strip.