Space-time integrals over growing time slabs #
The weak-continuity argument for the forced Leray--Hopf limit in
thm:leray-forced writes the change of a spatial pairing as a space-time
integral over K × (0,t). For an integrable density on K × (0,T) this
integral is the primitive of an integrable function of time, hence continuous
in t ∈ [0,T].
The CKN slab measure is the product of the restricted spatial and time measures.
theorem
CKN.Leray.forcedHopf_setIntegral_slab_eq_intervalIntegral
(K : Set Foundation.Parabolic.Vec3)
(T : ℝ)
(G : Foundation.Parabolic.ParabolicPoint → ℝ)
(hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T))))
(t : ℝ)
:
An integral over the growing slab K × (0,t) is the primitive of the
integrated spatial density.
theorem
CKN.Leray.forcedHopf_integrable_timeDensity
(K : Set Foundation.Parabolic.Vec3)
(T : ℝ)
(G : Foundation.Parabolic.ParabolicPoint → ℝ)
(hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T))))
:
MeasureTheory.Integrable ((Set.Ioo 0 T).indicator fun (τ : ℝ) => ∫ (x : Foundation.Parabolic.Vec3) in K, G (x, τ))
MeasureTheory.volume
The integrated spatial density of an integrable slab function is integrable in time.
theorem
CKN.Leray.forcedHopf_continuousOn_setIntegral_slab
(K : Set Foundation.Parabolic.Vec3)
(T : ℝ)
(G : Foundation.Parabolic.ParabolicPoint → ℝ)
(hG : MeasureTheory.Integrable G (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T))))
:
ContinuousOn (fun (t : ℝ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet K (Set.Ioo 0 t), G z)
(Set.Icc 0 T)
An integral over the growing slab K × (0,t) is continuous in
t ∈ [0,T].