L5 Serrin

Space-time L⁵ membership gives the finite branch of thm:lps at s = 5, where the time exponent is also five.

theorem ESS.lps_finite_branch_of_memLp_five {T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 5) ^ (2 * 5 / (5 - 3) / 5) < ⊤

Space-time L⁵ membership gives the finite branch of thm:lps at s = 5, where the time exponent is also five.