Cancellation of the cell scale in the concrete Riesz bound #
The parabolic Morrey normalization cancels the radius powers in both the near-source term and the annular tail. The resulting bound is independent of the centre, radius, and number of source annuli.
Time integration of the local concrete Riesz estimate #
The near-source estimate and the sum of exterior annuli give a bound on the time integral of the spatial operator norm. The constant is independent of the number of annuli used to cover the source.
theorem
CKN.Core.Step4.pressure_riesz_finite_annuli_time_bound
(i j : Fin 3)
{κ : ℝ}
(hκ : 0 < κ)
(hκhi : κ ≤ 25 / 9)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : AEMeasurable F MeasureTheory.volume)
(hFs :
∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
(x : Foundation.Parabolic.Vec3)
(t : ℝ)
{r : ℝ}
(hr : 0 < r)
(N : ℕ)
:
(∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, MeasureTheory.eLpNorm
(Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯
((Foundation.Parabolic.vec3Ball x (2 ^ N * (2 * r))).indicator fun (y : Foundation.Parabolic.Vec3) =>
F (y, s)))
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ^ (6 / 5)) ^ (5 / 6) ≤ ENNReal.ofReal (Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1) * (ENNReal.ofReal (2 * r) ^ (25 / 6 - 5 / κ) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F) + ENNReal.ofReal (6912 * (4 * Real.pi)⁻¹) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x r) ^ (5 / 6) * (ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 6) * ENNReal.ofReal (4 * r) ^ (5 / 3 - 5 / κ) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F * (1 - 2 ^ (-2 / 15))⁻¹)
Integrating the finite spatial decomposition gives the near and far terms with their exact cell-radius powers.
theorem
CKN.Core.Step4.pressure_riesz_finite_annuli_normalized_time_bound
(i j : Fin 3)
{κ : ℝ}
(hκ : 0 < κ)
(hκhi : κ ≤ 25 / 9)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : AEMeasurable F MeasureTheory.volume)
(hFs :
∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
(x : Foundation.Parabolic.Vec3)
(t : ℝ)
{r : ℝ}
(hr : 0 < r)
(N : ℕ)
:
ENNReal.ofReal r ^ (-(5 * (1 - 6 / 5 / κ) / (6 / 5))) * (∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, MeasureTheory.eLpNorm
(Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯
((Foundation.Parabolic.vec3Ball x (2 ^ N * (2 * r))).indicator fun (y : Foundation.Parabolic.Vec3) =>
F (y, s)))
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ^ (6 / 5)) ^ (5 / 6) ≤ (ENNReal.ofReal
(Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1) * 2 ^ (25 / 6 - 5 / κ) + ENNReal.ofReal (6912 * (4 * Real.pi)⁻¹) * ENNReal.ofReal (Real.pi * 4 / 3) * 4 ^ (5 / 3 - 5 / κ) * (1 - 2 ^ (-2 / 15))⁻¹) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F
The normalized temporal norm of every finite source decomposition is bounded independently of the cell and the number of annuli.