Solenoidal cutoff spatial limits

Spatial profile estimates and convergence for the Helmholtz cutoff potentials.

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

A time-compact spatial decay profile used to dominate the Helmholtz cutoff derivatives.

Equations

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

theorem CKN.Leray.associatedPressureSpatialProfile_memLp {K : Set ℝ} (hK : IsCompact K) {m r : ℝ} (hr : 0 < r) (hmr : 3 < m * r) : MeasureTheory.MemLp (associatedPressureSpatialProfile K m) (ENNReal.ofReal r) MeasureTheory.volume

The spatial decay profile belongs to L^r whenever its decay exponent beats the dimension.

theorem CKN.Leray.associatedPressurePotentialCutoff_hessian_profile_bound {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {K : Set ℝ} (hzero : ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), ψ (x, t) = 0) (hdecay : RieszPressurePotentialDecay ψ) (i j : Fin 3) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : |rieszPressureJointHessian (rieszPressurePotentialCutoffTest ψ n) i j z| ≤ (2 * Classical.choose ⋯ + 6 * cutoffGradientConstant * Classical.choose ⋯ + 9 * cutoffSecondDerivativeConstant * Classical.choose ⋯) * associatedPressureSpatialProfile K 2 z

Uniform spatial-profile control of the Hessian of a cutoff potential.

theorem CKN.Leray.associatedPressurePotentialCutoff_direction_profile_bound {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {K : Set ℝ} (hzero : ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), ψ (x, t) = 0) (hdecay : RieszPressurePotentialDecay ψ) (i : Fin 3) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : |rieszPressureJointDirection (rieszPressurePotentialCutoffTest ψ n) i z| ≤ (Classical.choose ⋯ + cutoffGradientConstant * Classical.choose ⋯) * associatedPressureSpatialProfile K 2 z

Uniform spatial-profile control of the gradient of a cutoff potential.

theorem CKN.Leray.associatedPressurePotentialCutoff_direction_eventually_eq {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, rieszPressureJointDirection (rieszPressurePotentialCutoffTest ψ n) i z = rieszPressureJointDirection ψ i z

At each fixed point, the cutoff potential gradient eventually agrees with the uncut gradient.

theorem CKN.Leray.associatedPressurePotentialCutoff_hessian_eq_of_inner {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (i j : Fin 3) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) (hxBall : z.1 ∈ euclideanBall 0 (rieszPressurePotentialCutoffScale n)) (hxClosed : z.1 ∈ euclideanClosedBall 0 (rieszPressurePotentialCutoffScale n)) : rieszPressureJointHessian (rieszPressurePotentialCutoffTest ψ n) i j z = rieszPressureJointHessian ψ i j z

The cutoff potential Hessian agrees with the original Hessian on the inner ball where the cutoff is constant.

theorem CKN.Leray.associatedPressureHelmholtzCutoffCurl_spatial_eventually_eq {T : ℝ} {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T)) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, spatialPartialProd (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl (associatedPressureHelmholtzCutoffVectorPotential φ n) w i) j z = spatialPartialProd (fun (w : Foundation.Parabolic.Vec3 × ℝ) => associatedPressureTestCurl (associatedPressureHelmholtzVectorPotential φ) w i) j z

Spatial derivatives of the cutoff curl eventually agree pointwise with those of the full Helmholtz curl.