Plateau of the short-time cutoff

In the spatial interior, after the lower-time transition, and above the phase gap, the compact cutoff is locally constant one.

def ESS.buShortCoreRegion (scale R ε : ℝ) : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)

The open plateau of the full compact cutoff.

Equations

• ESS.buShortCoreRegion scale R ε = {q : CKN.Foundation.Parabolic.Vec3 × ℝ | q.1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 R ∧ q ∈ ESS.buShortAboveGap scale ∧ 1 / 2 + 2 * ε < q.2}

theorem ESS.buShortCoreRegion_isOpen (scale R ε : ℝ) : IsOpen (buShortCoreRegion scale R ε)

The cutoff plateau is open.

theorem ESS.buShortFullCutoff_eq_one_on_core (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) : Set.EqOn (buShortFullCutoff scale R hR ε) (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => 1) (buShortCoreRegion scale R ε)

All three cutoff factors equal one on the plateau.

theorem ESS.buShortFullCutoff_derivatives_zero_on_core (scale R ε : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortCoreRegion scale R ε) : (∀ (j : Fin 3), CKN.spatialPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j z = 0) ∧ (∀ (j k : Fin 3), CKN.spatialSecondPartial (buCutScalar (buShortFullCutoff scale R hR ε)) j k z = 0) ∧ CKN.timePartial (buCutScalar (buShortFullCutoff scale R hR ε)) z = 0

The first, second, and time derivatives of the full cutoff vanish throughout its open plateau.