Uniform bounds for the forced quadratic pressure

eq:forced-pressure-bounds in lem:forced-energy-bounds, in the L^{3/2} form used on finite slabs: the quadratic part p_ε − p_f of the forced regularized pressure is the space-time Riesz pressure of J_ε u_ε ⊗ u_ε on the slab (prop:leray-pressure-limit), so the space-time Riesz bound eq:riesz-spacetime-bound and Hölder's inequality bound it by the L³ norms of the transport velocity and of the velocity. The L³ norm of the velocity is itself bounded by interpolation between L² and L^{10/3}.

theorem CKN.Leray.forcedLerayLimit_holder_three_three_threeHalves : ENNReal.HolderTriple 3 3 (ENNReal.ofReal (3 / 2))

theorem CKN.Leray.forcedLerayLimit_productPressure_eLpNorm_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))) : MeasureTheory.eLpNorm (lerayProductPressureOnSlab T v w hv hw) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ ENNReal.ofReal (rieszPressureOperatorBound (3 / 2) forcedLerayLimit_productPressure_eLpNorm_le._proof_1) * ∑ i : Fin 3, ∑ j : Fin 3, MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => v z i) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T)) * MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => w z j) 3 (MeasureTheory.volume.restrict (lerayPressureLimitSlab T))

eq:riesz-spacetime-bound for the product pressure on a finite slab: its L^{3/2} norm is at most the Riesz constant times the sum of the products of the L³ norms of the components of the two factors.

theorem CKN.Leray.forcedLerayLimit_lintegral_cube_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {g : α → ℝ} (hg : AEMeasurable g μ) : ∫⁻ (x : α), ‖g x‖ₑ ^ 3 ∂μ ≤ (∫⁻ (x : α), ‖g x‖ₑ ^ 2 ∂μ) ^ (1 / 4) * (∫⁻ (x : α), ‖g x‖ₑ ^ (10 / 3) ∂μ) ^ (3 / 4)

The L³ interpolation inequality between L² and L^{10/3}, in integral form: ∫|g|³ ≤ (∫|g|²)^{1/4} (∫|g|^{10/3})^{3/4}.

theorem CKN.Leray.forcedLerayLimit_uniform_slab_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) : ∃ (M3 : ENNReal) (MJ : ENNReal) (MP : ENNReal), M3 < ⊤ ∧ MJ < ⊤ ∧ MP < ⊤ ∧ ∀ (ε : ℝ) (hε : 0 < ε), (∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => forcedRegVelocity ρ a ha f hf ε z j) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ M3) ∧ (∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε) z i) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ≤ MJ) ∧ MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => forcedRegPressure ρ a ha f hf ε (Foundation.Parabolic.parabolicHomeomorph.symm z) - forcePressure f hf (Foundation.Parabolic.parabolicHomeomorph.symm z)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (lerayPressureLimitSlab T)) ≤ MP

Uniform slab bounds for the forced regularized solutions: on every finite slab the L³ norms of the velocity components and of the transport velocity components, and the L^{3/2} norm of the quadratic pressure, are bounded independently of ε (lem:forced-energy-bounds).

theorem CKN.Leray.forcedRegTransport_memLp_three_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) : MeasureTheory.MemLp (regUniformMollifiedVelocity ρ ε hε (forcedRegVelocity ρ a ha f hf ε)) 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

The transport velocity J_ε u_ε of a forced regularized solution lies in L³ on every finite slab (lem:forced-energy-bounds).