Vanishing normalized mass in the lower-time strip

The small-time trace estimate supplies two powers of the strip width. Absolute continuity of the time derivative's quadratic integral then removes the normalized lower-time cutoff error.

theorem ESS.bu_short_trace_strip_bound (B : Set CKN.Foundation.Parabolic.Vec3) (τ ε : ℝ) (hε : 0 < ε) (hετ : 2 * ε < τ) (f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal) (htrace : ∀ (t : ℝ), 0 < t → t < τ → ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, f (x, t) ≤ ENNReal.ofReal t * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ∫⁻ (s : ℝ) in Set.Ioc 0 t, g (x, s)) : ∫⁻ (t : ℝ) in Set.Ioc ε (2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, f (x, t) ≤ 2 * ENNReal.ofReal ε ^ 2 * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ∫⁻ (s : ℝ) in Set.Ioc 0 (2 * ε), g (x, s)

A sectionwise trace inequality bounds the mass of a time strip by its squared width times the derivative mass below the strip.

theorem ESS.bu_short_trace_strip_tendsto_zero (B : Set CKN.Foundation.Parabolic.Vec3) (τ : ℝ) (hτ : 0 < τ) (hBfinite : MeasureTheory.volume B < ⊤) (f g : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal) (hgmeas : AEMeasurable g ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)))) (hgfin : ∫⁻ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), g q ∂(MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)) < ⊤) (htrace : ∀ (t : ℝ), 0 < t → t < τ → ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, f (x, t) ≤ ENNReal.ofReal t * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ∫⁻ (s : ℝ) in Set.Ioc 0 t, g (x, s)) : Filter.Tendsto (fun (ε : ℝ) => (∫⁻ (t : ℝ) in Set.Ioc ε (2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, f (x, t)) / ENNReal.ofReal ε ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The normalized strip mass tends to zero when the time derivative has finite quadratic mass on the fixed spatial cylinder.