Weighted initial-time strip majorant

The weighted quadratic term generated by the lower-time cutoff is bounded by the normalized trace mass on the containing spatial ball.

theorem ESS.bu_short_early_weighted_majorant_le (scale R ε a Cw : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (hε : 0 < ε) (hCw : 0 ≤ Cw) (hweight : ∀ z ∈ buShortFixedCylinder R, buShortCarlemanWeight a z ≤ Cw) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (buCutSupportSet (buShortFullCutoff scale R hR ε)))) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (buCutSupportSet (buShortFullCutoff scale R hR ε)))) (hfInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (CKN.spaceTimeSet (buShortTraceBall R) (Set.Icc (1 / 2 + ε) (1 / 2 + 2 * ε))) MeasureTheory.volume) : have K := buCutSupportSet (buShortFullCutoff scale R hR ε); have S := CKN.spaceTimeSet (buShortTraceBall R) (Set.Icc (1 / 2 + ε) (1 / 2 + 2 * ε)); have f := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2; ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * (8 / ε) ^ 2 * S.indicator f z ≤ Cw * (8 / ε) ^ 2 * ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in buShortTraceBall R ×ˢ Set.Icc (1 / 2 + ε) (1 / 2 + 2 * ε), CKN.Foundation.Parabolic.vec3EuclideanNorm (v (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) ^ 2

The weighted quadratic mass of the shrinking strip is controlled by the quadratic trace mass on the larger ball.