Exchanging a spatial cutoff integral with a time integral #
A time-dependent density that agrees at almost every time with a jointly
strongly measurable density, and is dominated on the support of the spatial
cutoff by an integrable function of time, may be integrated first in space or
first in time. This is the exchange used for the mollified cross pairing in
lem:pv-serrin-uniqueness.
theorem
ESS.serrin_cutoff_fubini
{T t : ℝ}
(ht : t ∈ Set.Icc 0 T)
{η : CKN.Foundation.Parabolic.Vec3 → ℝ}
{K : Set CKN.Foundation.Parabolic.Vec3}
(hK : IsCompact K)
(hηK : ∀ y ∉ K, η y = 0)
(hηmeas : MeasureTheory.StronglyMeasurable η)
{Cη : ℝ}
(hηbd : ∀ (y : CKN.Foundation.Parabolic.Vec3), |η y| ≤ Cη)
{H : CKN.Foundation.Parabolic.Vec3 → ℝ → ℝ}
(hH :
MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × CKN.Foundation.Parabolic.Vec3) => H z.2 z.1)
((MeasureTheory.volume.restrict (Set.Ioo 0 T)).prod MeasureTheory.volume))
{m : ℝ → ℝ}
(hm : MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume)
(hbd : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ y ∈ K, |H y τ| ≤ m τ)
:
Fubini exchange for a cutoff-weighted density that is dominated by an integrable function of time on the cutoff support.