Riesz Second L2 Global Bounds

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Foundation.Euclidean.pressure_potential_tail_bound {G : Parabolic.Vec3 → ℝ} (hG : ContDiff ℝ (↑⊤) G) (hGc : HasCompactSupport G) {R : ℝ} (hR : 0 < R) (hSupp : tsupport G ⊆ Metric.closedBall 0 R) {x : Parabolic.Vec3} (hx : 2 * R ≤ ‖x‖) : |pressureNewtonianPotential G x| ≤ 2 * (4 * Real.pi)⁻¹ / ‖x‖ * ∫ (y : Parabolic.Vec3), |G y|

theorem CKN.Foundation.Euclidean.pressure_potential_compact_radius {F : Parabolic.Vec3 → ℝ} (hFc : HasCompactSupport F) : ∃ (R : ℝ), 0 < R ∧ 1 ≤ R ∧ tsupport F ⊆ Metric.closedBall 0 R

theorem CKN.Foundation.Euclidean.pressure_potential_deriv_tail_bound {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) {R : ℝ} (hR : 0 < R) (hSupp : tsupport F ⊆ Metric.closedBall 0 R) (i : Fin 3) {x : Parabolic.Vec3} (hx : 2 * R ≤ ‖x‖) : |spatialDeriv (pressureNewtonianPotential F) i x| ≤ 2 * (4 * Real.pi)⁻¹ / ‖x‖ * ∫ (y : Parabolic.Vec3), |spatialDeriv F i y|

noncomputable def CKN.Foundation.Euclidean.cutoffError (F : Parabolic.Vec3 → ℝ) {ρ : ℝ} (hρ : 0 < ρ) (x : Parabolic.Vec3) : ℝ

Error produced by applying the Laplacian to a cutoff Newtonian potential.

Equations

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

theorem CKN.Foundation.Euclidean.cutoffError_smooth {F : Parabolic.Vec3 → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hFc : HasCompactSupport F) {ρ : ℝ} (hρ : 0 < ρ) : ContDiff ℝ (↑⊤) (cutoffError F hρ)

theorem CKN.Foundation.Euclidean.cutoffError_hasCompactSupport {F : Parabolic.Vec3 → ℝ} {ρ : ℝ} (hρ : 0 < ρ) : HasCompactSupport (cutoffError F hρ)

noncomputable def CKN.Foundation.Euclidean.potentialTailSize (F : Parabolic.Vec3 → ℝ) : ℝ

Source and first-derivative mass controlling the tail of the Newtonian potential.

Equations

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

noncomputable def CKN.Foundation.Euclidean.cutoffErrorConstant (F : Parabolic.Vec3 → ℝ) : ℝ

Coefficient bounding the cutoff error in terms of source tail size.

Equations

• CKN.Foundation.Euclidean.cutoffErrorConstant F = 60 / 13 * CKN.Foundation.Euclidean.potentialTailSize F * (6 * CKN.cutoffGradientConstant + 3 * CKN.cutoffSecondDerivativeConstant)

theorem CKN.Foundation.Euclidean.potentialTailSize_nonneg {F : Parabolic.Vec3 → ℝ} : 0 ≤ potentialTailSize F

theorem CKN.Foundation.Euclidean.cutoffErrorConstant_nonneg {F : Parabolic.Vec3 → ℝ} : 0 ≤ cutoffErrorConstant F