Positive normal phase

The region where the normal phase exceeds its fixed threshold is open and lies in the plateau of the normal cutoff.

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

The open positive-phase region in the rescaled half-space strip.

Equations

• ESS.buShortPositivePhaseRegion scale = {z : CKN.Foundation.Parabolic.ParabolicPoint | 2 < z.1 2 ∧ 1 / 2 < z.2 ∧ z.2 < 1 ∧ ESS.buShortB scale < ESS.buShortFExt (z.1 2) z.2}

theorem ESS.buShortPositivePhaseRegion_isOpen (scale : ℝ) : IsOpen (buShortPositivePhaseRegion scale)

The positive-phase region is open.

theorem ESS.buShortPositivePhaseRegion_subset_aboveGap {scale : ℝ} (hscale : 0 < scale) : buShortPositivePhaseRegion scale ⊆ ⇑CKN.Foundation.Parabolic.parabolicHomeomorph ⁻¹' buShortAboveGap scale

Every positive-phase point lies above the completed normal cutoff transition.

theorem ESS.buShortShiftedWeight_zero_le_on_positive {scale a : ℝ} (ha : 0 ≤ a) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ buShortPositivePhaseRegion scale) : buShortShiftedWeight scale 0 z ≤ buShortShiftedWeight scale a z

On the positive phase, increasing a nonnegative Carleman parameter can only increase the shifted weight.

theorem ESS.buShortShiftedWeight_zero_continuousOn_positive (scale : ℝ) : ContinuousOn (buShortShiftedWeight scale 0) (buShortPositivePhaseRegion scale)

The phase-independent base of the shifted weight is continuous throughout the positive-phase region.

theorem ESS.buShortShiftedWeight_continuousOn_positive (scale a : ℝ) : ContinuousOn (buShortShiftedWeight scale a) (buShortPositivePhaseRegion scale)

The shifted half-space weight is continuous on the positive-phase region for every fixed Carleman parameter.