Serrin slices on a general time interval #
A finite mixed Serrin integral on (t₀, t₁) gives a finite spatial norm of
almost every time slice (lem:lps-H1-estimate).
theorem
ESS.lps_h1_finite_slice_memLp_ae
{t₀ t₁ s : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁))))
(hs : 3 < s)
(hmix :
∫⁻ (t : ℝ) in Set.Ioo t₀ t₁, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ t₁), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))
(ENNReal.ofReal s) MeasureTheory.volume
A finite mixed Serrin integral on (t₀, t₁) gives a finite spatial slice
norm at almost every time.