Mixed Norm Serrin #
The finite Serrin exponents satisfy the critical scaling relation in
thm:lps.
theorem
ESS.lps_finite_branch_slice_memLp_ae
{T s : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hs : 3 < s)
(hmix :
∫⁻ (t : ℝ) in Set.Ioo 0 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 0 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 gives a finite spatial slice norm at almost
every time, as used in thm:lps.
theorem
ESS.lps_finite_branch_time_moment_integrable
{T s : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hs : 3 < s)
(hmix :
∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤)
:
MeasureTheory.IntegrableOn
(fun (t : ℝ) =>
(MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))
(ENNReal.ofReal s) MeasureTheory.volume).toReal ^ (2 * s / (s - 3)))
(Set.Ioo 0 T) MeasureTheory.volume
The finite mixed Serrin integral makes the time power of the slice
L^s norm integrable, as used in thm:lps.