Vanishing of the lower-time cutoff contribution

The normalized quadratic trace estimate eliminates the weighted error caused by the derivative of the lower-time cutoff.

theorem ESS.bu_short_early_weighted_majorant_tendsto_zero (M scale R a : ℝ) (hM : 0 < M) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hR : 0 < R) (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)) (hinit : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0) (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 < ⊤) (hgrowth : ∀ 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)) : Filter.Tendsto (fun (ε : ℝ) => have K := buCutSupportSet (buShortFullCutoff scale R hR ε); have S := CKN.spaceTimeSet (buShortTraceBall R) (Set.Icc (1 / 2 + ε) (1 / 2 + 2 * ε)); have v := buAffineField (-scale ^ 2 / 2) scale w; 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) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The weighted initial-time strip majorant vanishes as the transition width tends to zero.