Integrability of the squared cutoff error comparison

The phase and shell majorants have finite integrals on each compact short-time cutoff support.

theorem ESS.bu_short_weighted_split_integrable (scale R ε c₁ C₁ C₂ a : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (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) (hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1)) (hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw) (hL2 : ∀ 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 < ⊤) : have K := buCutSupportSet (buShortFullCutoff scale R hR ε); have v := buAffineField (-scale ^ 2 / 2) scale w; have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw; MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (4 * buShortShiftedWeight scale a z * if z ∈ buShortWideGapRegion scale then buShortUniformErrorCoeff scale c₁ C₁ C₂ ^ 2 * (1 + z.1 2) ^ 4 else buShortShellCoeff scale R c₁ ^ 2) * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z) + 2 * buShortShiftedWeight scale a z * (if 1 / 2 + ε ≤ z.2 ∧ z.2 ≤ 1 / 2 + 2 * ε then 8 / ε * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) else 0) ^ 2) K MeasureTheory.volume

The squared phase, shell, and lower-time majorants are integrable on the support of a fixed short-time cutoff.