Decay estimates for compact Riesz potential approximations

This file proves the uniform integrable bounds and pointwise convergence used to extend pressure duality to decaying potential tests.

noncomputable def CKN.Leray.rieszPressurePotentialLaplacianCutoffError (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The Laplacian error introduced by the spatial cutoff, used by lem:riesz-duality.

Equations

• CKN.Leray.rieszPressurePotentialLaplacianCutoffError ψ n z = CKN.Leray.rieszPressureJointLaplacian (CKN.Leray.rieszPressurePotentialCutoffTest ψ n) z - CKN.Leray.rieszPressureJointLaplacian ψ z

noncomputable def CKN.Leray.rieszPressurePotentialHessianCutoffError (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (i j : Fin 3) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : ℝ

The Hessian error introduced by the spatial cutoff, used by lem:riesz-duality.

Equations

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

theorem CKN.Leray.rieszPressurePotentialCutoffTest_laplacian_formula {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : rieszPressureJointLaplacian (rieszPressurePotentialCutoffTest ψ n) z = rieszPressurePotentialCutoff n z.1 * rieszPressureJointLaplacian ψ z + 2 * spatialGradDot (rieszPressurePotentialCutoff n) (fun (x : Foundation.Parabolic.Vec3) => ψ (x, z.2)) z.1 + ψ z * spatialLaplacian (rieszPressurePotentialCutoff n) z.1

The spatial product rule for the cutoff Laplacian, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialCutoffTest_hessian_formula {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (n : ℕ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : rieszPressureJointHessian (rieszPressurePotentialCutoffTest ψ n) i j z = mixedSecond (rieszPressurePotentialCutoff n) i j z.1 * ψ z + spatialDeriv (rieszPressurePotentialCutoff n) j z.1 * rieszPressureJointDirection ψ i z + spatialDeriv (rieszPressurePotentialCutoff n) i z.1 * rieszPressureJointDirection ψ j z + rieszPressurePotentialCutoff n z.1 * rieszPressureJointHessian ψ i j z

The spatial product rule for a cutoff Hessian component, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialDecay_hessian_bound_norm {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hdecay : RieszPressurePotentialDecay ψ) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : |rieszPressureJointHessian ψ i j z| ≤ Classical.choose ⋯ * (1 + ‖z.1‖) ^ (-4)

The Hessian decay bound in the CKN Euclidean norm, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialDecay_laplacian_bound_norm {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hdecay : RieszPressurePotentialDecay ψ) (z : Foundation.Parabolic.Vec3 × ℝ) : |rieszPressureJointLaplacian ψ z| ≤ 3 * Classical.choose ⋯ * (1 + ‖z.1‖) ^ (-4)

The Laplacian decay bound in the CKN Euclidean norm, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressureJointHessian_zero_of_slice_zero {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) {z : Foundation.Parabolic.Vec3 × ℝ} (hzero : (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) = fun (x : Foundation.Parabolic.Vec3) => 0) (i j : Fin 3) : rieszPressureJointHessian f i j z = 0

A smooth potential with a zero spatial slice has zero spatial Hessian on that slice, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressureJointLaplacian_zero_of_slice_zero {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) {z : Foundation.Parabolic.Vec3 × ℝ} (hzero : (fun (x : Foundation.Parabolic.Vec3) => f (x, z.2)) = fun (x : Foundation.Parabolic.Vec3) => 0) : rieszPressureJointLaplacian f z = 0

A smooth potential with a zero spatial slice has zero spatial Laplacian on that slice, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialHessianCutoffError_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 × ℝ) : |rieszPressurePotentialHessianCutoffError ψ i j n z| ≤ (Classical.choose ⋯ + 6 * cutoffGradientConstant * Classical.choose ⋯ + 9 * cutoffSecondDerivativeConstant * Classical.choose ⋯) * rieszPressurePotentialSpatialProfile K z

A uniform spatially integrable bound for the cutoff Hessian error, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressurePotentialLaplacianCutoffError_bound {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {K : Set ℝ} (hzero : ∀ t ∉ K, ∀ (x : Foundation.Parabolic.Vec3), ψ (x, t) = 0) (hdecay : RieszPressurePotentialDecay ψ) (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) : |rieszPressurePotentialLaplacianCutoffError ψ n z| ≤ (3 * Classical.choose ⋯ + 18 * cutoffGradientConstant * Classical.choose ⋯ + 27 * cutoffSecondDerivativeConstant * Classical.choose ⋯) * rieszPressurePotentialSpatialProfile K z

A uniform spatially integrable bound for the cutoff Laplacian error, used by lem:riesz-duality.