Absolute continuity on shrinking time strips #
An integrable nonnegative space-time function has vanishing integral on bounded spatial sets as the time strip shrinks to the initial face.
theorem
ESS.bu_short_product_measure_shrinking
(B : Set CKN.Foundation.Parabolic.Vec3)
(τ : ℝ)
(hBfinite : MeasureTheory.volume B < ⊤)
:
Filter.Tendsto
(fun (ε : ℝ) =>
((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)))
(Set.univ ×ˢ Set.Ioc 0 (2 * ε)))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Product volume of a bounded spatial set and a shrinking initial-time strip tends to zero.
theorem
ESS.bu_short_product_lintegral_shrinking
(B : Set CKN.Foundation.Parabolic.Vec3)
(τ : ℝ)
(hBfinite : MeasureTheory.volume B < ⊤)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal)
(hf :
∫⁻ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), f q ∂(MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)) < ⊤)
:
Filter.Tendsto
(fun (ε : ℝ) =>
∫⁻ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in Set.univ ×ˢ Set.Ioc 0 (2 * ε), f q ∂(MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)))
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Finite product-space mass vanishes on the shrinking time strip.
theorem
ESS.bu_short_nested_lintegral_shrinking
(B : Set CKN.Foundation.Parabolic.Vec3)
(τ : ℝ)
(hτ : 0 < τ)
(hBfinite : MeasureTheory.volume B < ⊤)
(f : CKN.Foundation.Parabolic.Vec3 × ℝ → ENNReal)
(hfmeas : AEMeasurable f ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ))))
(hf :
∫⁻ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), f q ∂(MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ)) < ⊤)
:
Tonelli gives the same shrinking limit with space integrated outside time, as in the small-time trace estimate.