The local L^{3/2} bound for mixed-norm pressures

A space-time function in L²_t L⁶_x is locally in L^{3/2}: on a bounded cylinder K × J, the finite-measure embeddings L⁶(K) ⊂ L^{3/2}(K) and L²(J) ⊂ L^{3/2}(J) give eq:force-pressure-local.

theorem CKN.Leray.measurable_eLpNorm_slice {P : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hP : MeasureTheory.StronglyMeasurable P) {p : ENNReal} (hp0 : p ≠ 0) (hptop : p ≠ ⊤) (μ : MeasureTheory.Measure Foundation.Parabolic.Vec3) [MeasureTheory.SFinite μ] : Measurable fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) p μ

The L^p norm of the time slices of a strongly measurable space-time function is measurable in time.

theorem CKN.Leray.eLpNorm_threeHalves_cylinder_le {P : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hP : MeasureTheory.StronglyMeasurable P) {T : ℝ} (K : Set Foundation.Parabolic.Vec3) {I : Set ℝ} (hIT : I ⊆ Set.Ioo 0 T) : MeasureTheory.eLpNorm P (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (K ×ˢ I)) ≤ MeasureTheory.volume K ^ (1 / 2) * MeasureTheory.volume I ^ (1 / 6) * (∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => P (x, t)) (ENNReal.ofReal 6) MeasureTheory.volume ^ 2) ^ (1 / 2)

The local bound eq:force-pressure-local: on a cylinder K × J inside the slab (0, T), the L^{3/2} norm is at most |K|^{1/2} |J|^{1/6} times the L²_t L⁶_x norm on the slab.