Decaying potential tests for pressure duality

The derivative bounds in RieszPressurePotentialDecay are the componentwise form of eq:riesz-potential-decay.

structure CKN.Leray.RieszPressurePotentialDecay (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : Prop

Uniform spatial decay and compact time support for the potential tests in lem:riesz-duality.

• timeSupport : ∃ (K : Set ℝ), IsCompact K ∧ ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), ψ (x, t) = 0
• value_bound : ∃ C ≥ 0, ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |ψ z| ≤ C * (1 + Foundation.Parabolic.vec3EuclideanNorm z.1) ^ (-2)
• gradient_bound : ∃ C ≥ 0, ∀ (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ), |rieszPressureJointDirection ψ i z| ≤ C * (1 + Foundation.Parabolic.vec3EuclideanNorm z.1) ^ (-3)
• hessian_bound : ∃ C ≥ 0, ∀ (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ), |rieszPressureJointHessian ψ i j z| ≤ C * (1 + Foundation.Parabolic.vec3EuclideanNorm z.1) ^ (-4)

noncomputable def CKN.Leray.rieszPressurePotentialSpatialProfile (K : Set ℝ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The common space-time (L^3) majorant for derivatives of a decaying potential test, used by lem:riesz-duality.

Equations

• CKN.Leray.rieszPressurePotentialSpatialProfile K z = K.indicator (fun (x : ℝ) => 1) z.2 * (1 + ‖z.1‖) ^ (-4)

theorem CKN.Leray.rieszPressurePotentialSpatialProfile_memLp3 {K : Set ℝ} (hK : IsCompact K) : MeasureTheory.MemLp (rieszPressurePotentialSpatialProfile K) (ENNReal.ofReal 3) MeasureTheory.volume

The potential-test majorant is in space-time (L^3), used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotential_memLp3_of_decay {K : Set ℝ} (hK : IsCompact K) {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : Continuous f) (C : ℝ) (hC : 0 ≤ C) (hzero : ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), f (x, t) = 0) (hbound : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), |f z| ≤ C * (1 + Foundation.Parabolic.vec3EuclideanNorm z.1) ^ (-4)) : MeasureTheory.MemLp f (ENNReal.ofReal 3) MeasureTheory.volume

A continuous function with fourth-order spatial decay and compact time support belongs to space-time (L^3), used by lem:riesz-duality.

theorem CKN.Leray.rieszPressureJointLaplacian_memLp3 {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hdecay : RieszPressurePotentialDecay ψ) : MeasureTheory.MemLp (rieszPressureJointLaplacian ψ) (ENNReal.ofReal 3) MeasureTheory.volume

The spatial Laplacian test in lem:riesz-duality belongs to space-time L^3, used by the noncompact-potential identity.