Phase gap for cutoff derivatives

The normal-phase factor of the cutoff is locally one above the fixed negative phase gap. Its derivative errors therefore lie below that gap.

def ESS.buShortAboveGap (scale : ℝ) : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)

The open region above the negative transition gap where the normal cutoff has completed its transition.

Equations

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

theorem ESS.buShortAboveGap_isOpen (scale : ℝ) : IsOpen (buShortAboveGap scale)

The region above the negative phase gap is open.

theorem ESS.buShortEtaExt_eq_one_on_aboveGap {scale : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) : Set.EqOn (buShortEtaExt scale) (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 1) (buShortAboveGap scale)

The smooth normal cutoff is one throughout the region above the gap.

theorem ESS.buShortEtaExt_derivatives_zero_aboveGap {scale : ℝ} (hscale : 0 < scale) (hscale1 : scale ≤ 1) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale) : (∀ (j : Fin 3), CKN.spatialPartial (buCutScalar (buShortEtaExt scale)) j z = 0) ∧ (∀ (j k : Fin 3), CKN.spatialSecondPartial (buCutScalar (buShortEtaExt scale)) j k z = 0) ∧ CKN.timePartial (buCutScalar (buShortEtaExt scale)) z = 0

On the region above the gap, every first, second spatial, and time derivative of the normal cutoff vanishes.