Real-valued version of the normalized trace limit #
The nonnegative extended-real strip estimate transfers to a real set integral. This is the form used by the absorbed Carleman inequality.
theorem
ESS.bu_short_real_strip_of_lintegral_limit
(B : Set CKN.Foundation.Parabolic.Vec3)
(σ τ : ℝ)
(hτ : 0 < τ)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hfmeas :
MeasureTheory.AEStronglyMeasurable f
((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo σ (σ + τ)))))
(hf0 : ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ f q)
(hH :
Filter.Tendsto
(fun (ε : ℝ) =>
(∫⁻ (t : ℝ) in Set.Ioc (σ + ε) (σ + 2 * ε), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ENNReal.ofReal (f (x, t))) / ENNReal.ofReal ε ^ 2)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0))
:
A normalized extended-real strip limit transfers to a real set integral when the integrand is nonnegative and measurable.
theorem
ESS.bu_short_real_trace_strip_tendsto_zero
(B : Set CKN.Foundation.Parabolic.Vec3)
(τ : ℝ)
(hτ : 0 < τ)
(hBfinite : MeasureTheory.volume B < ⊤)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hfmeas :
MeasureTheory.AEStronglyMeasurable f
((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ))))
(hf0 : ∀ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ f q)
(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, ENNReal.ofReal (f (x, t)) ≤ ENNReal.ofReal t * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ∫⁻ (s : ℝ) in Set.Ioc 0 t, g (x, s))
:
A sectionwise trace estimate and finite time-derivative mass imply vanishing normalized real quadratic mass on a bounded spatial set.