The positive-time L² pressure estimate for regularized solutions

The slice pressure is the double Riesz transform of the regularized tensor. This file bounds that pressure class by the two spatial L⁴ norms in lem:reg-pressure-L2.

noncomputable def CKN.Leray.regPressureTensorSlice (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : ℝ

The tensor in the Riesz pressure formula for a regularized velocity.

Equations

• CKN.Leray.regPressureTensorSlice ρ ε hε u t i j x = CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j

theorem CKN.Leray.regPressure_slice_L2_bound (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (P : ℝ → ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal 2) MeasureTheory.volume)) (hU2 : ∀ (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (regUniformVelocitySlice u t) 2 MeasureTheory.volume) (hUbound : ∀ (t : ℝ), 0 < t → ∃ (B : ℝ), 0 ≤ B ∧ ∀ (x : Foundation.Parabolic.Vec3), Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ B) (hR4 : ∀ (t : ℝ), 0 < t → ∃ (F : PressureTensorLp 2), (∀ (i j : Fin 3), ↑↑(F i j) =ᵐ[MeasureTheory.volume] regPressureTensorSlice ρ ε hε u t i j) ∧ P t = rieszPressureSlice 2 regPressure_slice_L2_bound._proof_1 F) (t : ℝ) : 0 < t → ‖P t‖ ≤ 9 * rieszPressureOperatorBound 2 regPressure_slice_L2_bound._proof_1 * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedVelocity ρ ε hε u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) (ENNReal.ofReal 4) MeasureTheory.volume).toReal

The positive-time Riesz pressure is bounded in L² by the two L⁴ norms in lem:reg-pressure-L2. The pressure binder is exactly the (R4) slice identity in the L² realization of the double Riesz transform.