Integrating phase and shell errors

An integrable Gaussian majorant controls the negative-phase error, while a fixed-parameter weighted energy controls the spatial shell.

theorem ESS.bu_short_split_integral_le_global (K G H : Set CKN.Foundation.Parabolic.ParabolicPoint) (hK : MeasurableSet K) (hG : MeasurableSet G) (hH : MeasurableSet H) (hKH : K ⊆ H) (hGH : G ⊆ H) (W T P Q B : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (C₁ C₂ e : ℝ) (hW : ∀ z ∈ H, 0 ≤ W z) (hP : ∀ z ∈ H, 0 ≤ P z) (hQ : ∀ z ∈ H, 0 ≤ Q z) (hgap : ∀ z ∈ G, W z ≤ e * T z) (hWP : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * P z * Q z) H MeasureTheory.volume) (hWQ : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * Q z) H MeasureTheory.volume) (hTPQ : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => T z * P z * Q z) G MeasureTheory.volume) (hB : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * B z ^ 2) K MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, (4 * W z * if z ∈ G then C₁ ^ 2 * P z else C₂ ^ 2) * Q z + 2 * W z * B z ^ 2 ≤ ((4 * C₁ ^ 2 * e * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in G, T z * P z * Q z) + 4 * C₂ ^ 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in H, W z * Q z) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, W z * B z ^ 2

A phase-gap majorant and an integrable global energy bound control the phase and shell terms on any smaller cutoff support.