The L^{5/3} bound for the forced quadratic pressure

eq:forced-ten-thirds and eq:forced-pressure-bounds in lem:forced-energy-bounds, in the L^{5/3} form: the transport velocity J_ε u_ε of a forced regularized solution obeys the same uniform L^{10/3} bound on finite slabs as the velocity (Young's inequality for the mollifier), so the quadratic tensor J_ε u_ε ⊗ u_ε is uniformly in L^{5/3} on the slab, and the L^{5/3} space-time Riesz bound of def:riesz-pressure gives a uniform L^{5/3} bound for the quadratic pressure p_ε − p_f.

theorem CKN.Leray.forcedLerayLimit_productPressure_eLpNorm_fiveThirds_le (T : ℝ) (v w : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : MeasureTheory.MemLp v 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hw : MeasureTheory.MemLp w 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hv' : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) (hw' : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => w z j) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))) : MeasureTheory.eLpNorm (lerayProductPressureOnSlab T v w hv hw) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal (rieszPressureOperatorBound (5 / 3) forcedLerayLimit_productPressure_eLpNorm_fiveThirds_le._proof_1) * ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T)) * MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => w z j) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))

eq:riesz-spacetime-bound in L^{5/3} for the product pressure on a finite slab: when both factors are in L^{10/3} on the slab, the product pressure is bounded in L^{5/3} by the Riesz constant times the products of the L^{10/3} norms of the components.

theorem CKN.Leray.forcedLerayLimit_fiveThirds_bounds (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (T : ℝ) (hT : 0 < T) : ∃ (M : ENNReal) (MJ : ENNReal) (MP : ENNReal), M < ⊤ ∧ MJ < ⊤ ∧ MP < ⊤ ∧ ∀ (ε : ℝ) (hε : 0 < ε), (∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => forcedRegVelocity ρ a ha f hf ε z j) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ M) ∧ (∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z i) (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ MJ) ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => forcedRegPressure ρ a ha f hf ε z - forcePressure f hf z) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ MP

eq:forced-ten-thirds and the L^{5/3} part of eq:forced-pressure-bounds in lem:forced-energy-bounds: on a finite slab the velocity and the transport velocity of the forced regularized solutions are bounded in L^{10/3}, and the quadratic pressure p_ε − p_f in L^{5/3}, uniformly in ε.