The distributional sign of pressure

The pressure convention in def:riesz-pressure is the negative of CKN's raw second derivative operator.

noncomputable def CKN.Leray.rieszPressureRawExtensionInput (r : ℝ) (hr : 1 < r) (i j : Fin 3) : Foundation.Euclidean.LpExtensionInput (ENNReal.ofReal r) (rieszPressureOperatorBound r hr)

The raw L^r extension input for the i,j Riesz pressure component.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.rieszPressureOperator_laplacian_pairing_of_memLp (r : ℝ) (hr : 1 < r) (i j : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) (hgr : MeasureTheory.MemLp g (ENNReal.ofReal r) MeasureTheory.volume) (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), ↑↑((rieszPressureOperator r hr i j) (MeasureTheory.MemLp.toLp g hgr)) x * spatialLaplacian ψ x = -∫ (x : Foundation.Parabolic.Vec3), g x * mixedSecond ψ i j x

The signed Laplacian pairing holds on the full L^r domain.

theorem CKN.Leray.rieszPressureSlice_laplacian_identity_of_memLp (r : ℝ) (hr : 1 < r) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), ↑↑(rieszPressureSlice r hr fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (F i j) ⋯) x * -spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), F i j x * mixedSecond ψ i j x