Identification of the quadratic pressure

The frequency pressure of a real tensor field satisfies the Laplacian identity of the Riesz pressure; their difference is square integrable and weakly harmonic, hence zero by Liouville's theorem. This identifies the pressure of lem:regularised-forced with its frequency representation in the pressure pairing of eq:reg-momentum-forced.

noncomputable def CKN.Leray.gradField (ψ : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The gradient of a scalar test as a vector test.

Equations

• CKN.Leray.gradField ψ x k = CKN.spatialDeriv ψ k x

theorem CKN.Leray.gradField_contDiff {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : ContDiff ℝ (↑⊤) (gradField ψ)

theorem CKN.Leray.gradField_hasCompactSupport {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψc : HasCompactSupport ψ) : HasCompactSupport (gradField ψ)

theorem CKN.Leray.fourier_testField_gradField {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (ξ : Foundation.Parabolic.L2Vec3) : FourierTransform.fourier (testField (gradField ψ)) ξ = (2 * ↑Real.pi * Complex.I * FourierTransform.fourier (scalTestField ψ) ξ) • complexifyFrequency ξ

theorem CKN.Leray.integrable_forcedTensorComp_mul (T : ↥RealTensorL2) (i j : Fin 3) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => forcedTensorComp T i j x * g x) MeasureTheory.volume

theorem CKN.Leray.integral_quadPressureTilde_laplacian (T : ↥RealTensorL2) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), quadPressureTilde T x * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), forcedTensorComp T i j x * mixedSecond ψ i j x

The Laplacian identity of the frequency pressure.

theorem CKN.Leray.lpNorm_threeHalves_ball_le {H : Foundation.Parabolic.Vec3 → ℝ} (hH : MeasureTheory.MemLp H 2 MeasureTheory.volume) {ρ : ℝ} (hρ : 0 < ρ) : MeasureTheory.MemLp H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ∧ MeasureTheory.lpNorm H (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ MeasureTheory.lpNorm H 2 MeasureTheory.volume * (1 + ρ)

A square-integrable function has at most linear growth of its local L^{3/2} norms on balls.

theorem CKN.Leray.rieszPressure_ae_eq_quadPressureTilde (T : ↥RealTensorL2) : rieszPressureSliceRepresentative 2 rieszPressure_ae_eq_quadPressureTilde._proof_1 (forcedPressureTensorLp T) =ᵐ[MeasureTheory.volume] quadPressureTilde T

The Riesz pressure of a real tensor field is its frequency pressure.