Negative-phase bound on compact positive-phase sets

Removing the lower-time and spatial cutoffs leaves only the exponentially small negative-phase integral.

theorem ESS.bu_short_compact_mass_le_gap : ∃ (a₀ : ℝ) (c : ℝ), 0 < a₀ ∧ 0 < c ∧ ∀ (M scale c₁ C₁ C₂ a : ℝ), 0 < M → 0 < scale → scale ≤ 1 → 0 ≤ c₁ → 0 ≤ C₁ → (∀ (scale y : ℝ), |deriv (deriv (buShortNormalCutoff scale)) y| ≤ C₁) → 0 ≤ C₂ → (∀ (x : ℝ), |deriv (deriv CKN.smoothTransitionProfile) x| ≤ C₂) → c * 36 * (c₁ * scale) ^ 2 ≤ 1 / 2 → max a₀ 1 < a → ∀ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) → (∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) → CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw → (∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) → (∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z))) → (∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)) → MeasureTheory.IntegrableOn (buShortTangentialDensity scale w Dw) (buShortWideGapRegion scale) MeasureTheory.volume → MeasureTheory.IntegrableOn (buShortWeightedPolynomialDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume → MeasureTheory.IntegrableOn (buShortWeightedDensity scale a w Dw) (buShortHighStrip scale) MeasureTheory.volume → ∀ (S : Set CKN.Foundation.Parabolic.ParabolicPoint), IsCompact S → S.Nonempty → (∀ z ∈ S, CKN.Foundation.Parabolic.parabolicHomeomorph z ∈ buShortAboveGap scale) → have v := buAffineField (-scale ^ 2 / 2) scale w; ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, buShortShiftedWeight scale a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ 16 * c * buShortUniformErrorCoeff scale c₁ C₁ C₂ ^ 2 * Real.exp (-(a * buShortD scale)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in buShortWideGapRegion scale, buShortTangentialDensity scale w Dw z

A compact set in the normal cutoff plateau has only the negative-phase contribution after both compact cutoffs are removed.