The Riesz pressure identity (R4)

For any velocity whose slices represent a curve U of spatial L² fields, the canonical pressure forcedQuadPressure of U is, on each slice, the Riesz pressure of the regularized tensor (J_ε u)_i u_j, and it satisfies the Laplacian identity of thm:regularised (R4).

theorem CKN.Leray.regR12_R4 (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (U : ℝ → ↥RealVectorL2) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (t : ℝ) (hrep : (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) =ᵐ[MeasureTheory.volume] realVectorL2Representative (U t)) : ∃ (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) (ENNReal.ofReal 2) MeasureTheory.volume), ((fun (x : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε U (x, t)) =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 regR12_R4._proof_1 fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j) ⋯) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), forcedQuadPressure ρ ε hε U (x, t) * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), regUniformMollifiedVelocity ρ ε hε u (x, t) i * u (x, t) j * mixedSecond ψ i j x

thm:regularised (R4) for a velocity whose slices represent a curve.