Space-time integrability of the forced regularized solutions

eq:forced-ten-thirds in lem:forced-energy-bounds: on every finite slab the forced regularized velocity lies in L^{10/3}, with a bound depending only on the constants E_T and G_T of the uniform energy bounds, and hence, by interpolation with L², in L³. The slice interpolation estimate is integrated in time on the slab (0,T) by applying the positive-time estimate to the velocity truncated at time T.

theorem CKN.Leray.forcedLerayLimit_component_tenThirds_slab (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (A D : ENNReal) (T : ℝ) (hSlices : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∃ (h : Fin 3 → H1Function Set.univ), (∀ (i : Fin 3) (x : Vec 3), (h i).toFun x = u (x, t) i) ∧ ∀ (i : Fin 3) (x : Vec 3) (j : Fin 3), (h i).grad x j = Du (x, t) i j) (hSliceBound : ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume ≤ A) (hUmeasurable : Measurable u) (hDumeasurable : Measurable Du) (hGradientBound : ∫⁻ (t : ℝ) in Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (spatialGradientSq u Du (x, t)) ≤ D) (hAfinite : A < ⊤) (hDfinite : D < ⊤) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ^ (10 / 3) ≤ (gagliardoNirenbergSobolevConstant ^ (3 / 5)) ^ (10 / 3) * A ^ (4 / 3) * D

The space-time L^{10/3} estimate on the finite slab (0,T): slices in H¹ with a uniform L² bound A and a gradient bound D on the slab give L^{10/3} on the slab, component by component, with the constant of the positive-time estimate.

theorem CKN.Leray.forcedRegVelocity_memLp_slab (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (ε : ℝ) (hε : 0 < ε) (T : ℝ) (hT : 0 < T) : have μ := MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)); have E := Real.exp T * ((∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z i ^ 2); have G := (((∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2) + ∑ i : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), f z i ^ 2) + T * E) / 2; MeasureTheory.MemLp (forcedRegVelocity ρ a ha f hf ε) 2 μ ∧ MeasureTheory.MemLp (forcedRegVelocity ρ a ha f hf ε) (ENNReal.ofReal (10 / 3)) μ ∧ MeasureTheory.MemLp (forcedRegVelocity ρ a ha f hf ε) 3 μ ∧ ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => forcedRegVelocity ρ a ha f hf ε z i) (ENNReal.ofReal (10 / 3)) μ ^ (10 / 3) ≤ (gagliardoNirenbergSobolevConstant ^ (3 / 5)) ^ (10 / 3) * ENNReal.ofReal √E ^ (4 / 3) * ENNReal.ofReal G

eq:forced-ten-thirds: on every finite slab the forced regularized velocity lies in L², L^{10/3} and L³, and each component obeys the L^{10/3} bound in terms of the constants E_T and G_T² of lem:forced-energy-bounds, which do not depend on ε.