Space-time pressure bounds for the regularized tensor

The Riesz pressure operator transfers the L^{5/3} tensor estimate to pressure. On a finite time slab, interpolation between the tensor L¹ and L^{5/3} estimates gives the L^{3/2} pressure bound.

def CKN.Leray.regPressureSpaceTimeTensor (J U : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ

The regularized transport tensor in space-time coordinates, used by def:riesz-pressure.

Equations

• CKN.Leray.regPressureSpaceTimeTensor J U i j z = J z i * U z j

theorem CKN.Leray.regPressure_regularized_fiveThirds_bound (J U : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hJ : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J z i) (ENNReal.ofReal (10 / 3)) MeasureTheory.volume) (hU : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => U z j) (ENNReal.ofReal (10 / 3)) MeasureTheory.volume) (BJ BU : ℝ) (hBJ : 0 ≤ BJ) (hBU : 0 ≤ BU) (hJbound : ∀ (i : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => J z i) (ENNReal.ofReal (10 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal BJ) (hUbound : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => U z j) (ENNReal.ofReal (10 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal BU) : ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (regPressureSpaceTimeTensor J U i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume), ‖rieszPressureSpaceTimeClass (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 (rieszPressureSpaceTimeTensorToLp (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 (regPressureSpaceTimeTensor J U) hF)‖ ≤ 9 * rieszPressureOperatorBound (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 * (BJ * BU)

The global tensor L^{5/3} estimate follows from the two velocity L^{10/3} bounds in lem:reg-ten-thirds.

theorem CKN.Leray.regPressure_spaceTime_fiveThirds_norm_bound (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) (M : ℝ) (hM : 0 ≤ M) (hFbound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal M) : ‖rieszPressureSpaceTimeClass (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 (rieszPressureSpaceTimeTensorToLp (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 F hF)‖ ≤ 9 * rieszPressureOperatorBound (5 / 3) regPressure_regularized_fiveThirds_bound._proof_1 * M

The global L^{5/3} pressure class is bounded by the componentwise L^{5/3} size of the regularized tensor, as in lem:reg-pressure-bound.

theorem CKN.Leray.regPressure_spaceTime_threeHalves_norm_bound (T A M : ℝ) (hT : 0 ≤ T) (hA : 0 ≤ A) (hM : 0 ≤ M) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF1 : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal 1) MeasureTheory.volume) (hF53 : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) (hF1bound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (F i j) (ENNReal.ofReal 1) MeasureTheory.volume ≤ ENNReal.ofReal (T * A)) (hF53bound : ∀ (i j : Fin 3), MeasureTheory.eLpNorm (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume ≤ ENNReal.ofReal M) : ∃ (hF32 : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume), ‖rieszPressureSpaceTimeClass (3 / 2) regPressure_spaceTime_threeHalves_norm_bound._proof_1 (rieszPressureSpaceTimeTensorToLp (3 / 2) regPressure_spaceTime_threeHalves_norm_bound._proof_1 F hF32)‖ ≤ 9 * rieszPressureOperatorBound (3 / 2) regPressure_spaceTime_threeHalves_norm_bound._proof_1 * ((T * A) ^ (1 / 6) * M ^ (5 / 6))

On a finite slab, interpolation of the tensor L¹ and L^{5/3} bounds gives the L^{3/2} pressure estimate in lem:reg-pressure-bound. The tensor is the one in the (R4) pressure formula, restricted to that slab.