Finite annular decomposition of the pressure Riesz operator

A source restricted to a large ball is split into its near part and finitely many dyadic annuli. The near part uses the global Calderón–Zygmund bound; each annulus uses the exterior inverse-cube estimate.

Exterior Riesz estimates for spatial annuli

An annulus outside twice the observation radius is separated from the observation ball. The exterior formula for the concrete pressure operator then supplies its inverse-cube source estimate.

theorem CKN.Core.Step4.pressure_source_annulus_hasCompactSupport (G : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) : HasCompactSupport ((Foundation.Parabolic.vec3Ball x (2 * ρ) \ Foundation.Parabolic.vec3Ball x ρ).indicator G)

A source restricted to a bounded spatial annulus has compact support.

theorem CKN.Core.Step4.pressure_riesz_annulus_enorm_bound (i j : Fin 3) {G : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) {r ρ : ℝ} (hr : 0 < r) (hrρ : 2 * r ≤ ρ) : ∀ᵐ (y : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r), ‖Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ ((Foundation.Parabolic.vec3Ball x (2 * ρ) \ Foundation.Parabolic.vec3Ball x ρ).indicator G) y‖ₑ ≤ ENNReal.ofReal (6912 * (4 * Real.pi)⁻¹) * ENNReal.ofReal (2 * ρ) ^ (-3) * ∫⁻ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * ρ), ‖G z‖ₑ

The annular component of the concrete Riesz operator has a pointwise bound on a smaller ball, with an explicit inverse-cube scale factor.

theorem CKN.Core.Step4.pressure_riesz_annulus_eLpNorm_bound (i j : Fin 3) {G : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) {r ρ : ℝ} (hr : 0 < r) (hrρ : 2 * r ≤ ρ) : MeasureTheory.eLpNorm (Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ ((Foundation.Parabolic.vec3Ball x (2 * ρ) \ Foundation.Parabolic.vec3Ball x ρ).indicator G)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ (ENNReal.ofReal (6912 * (4 * Real.pi)⁻¹) * ENNReal.ofReal (2 * ρ) ^ (-3) * ∫⁻ (z : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * ρ), ‖G z‖ₑ) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x r) ^ (5 / 6)

The pointwise annular estimate gives its local L^{6/5} bound, retaining the observation ball's volume factor.

theorem CKN.Core.Step4.pressure_riesz_finite_annuli_eLpNorm_bound (i j : Fin 3) {G : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (x : Foundation.Parabolic.Vec3) {r : ℝ} (hr : 0 < r) (N : ℕ) : MeasureTheory.eLpNorm (Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ ((Foundation.Parabolic.vec3Ball x (2 ^ N * (2 * r))).indicator G)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ ENNReal.ofReal (Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1) * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (2 * r))) + ENNReal.ofReal (6912 * (4 * Real.pi)⁻¹) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x r) ^ (5 / 6) * ∑ n ∈ Finset.range N, ENNReal.ofReal (2 * (2 ^ n * (2 * r))) ^ (-3) * ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * (2 ^ n * (2 * r))), ‖G y‖ₑ

The local norm of a source restricted to a dyadic outer ball is bounded by its near norm and the finite sum of exterior source masses.