Local pieces of the concrete pressure Riesz operator #
The concrete operator has its global L^{6/5} bound and respects a spatial
near/far decomposition. Away from the support its exterior formula gives a
pointwise bound by the source's spatial L^1 norm.
theorem
CKN.Core.Step4.pressure_riesz_component_eLpNorm_bound
(i j : Fin 3)
{G : Foundation.Parabolic.Vec3 → ℝ}
(hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
(hGc : HasCompactSupport G)
:
MeasureTheory.eLpNorm
(Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ G)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal (Foundation.Euclidean.czGradientComponentConstant Foundation.Euclidean.rieszSecondWeakTypeConstant 1) * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume
The concrete component operator has a fixed global L^{6/5} bound.
theorem
CKN.Core.Step4.pressure_riesz_component_indicator_add_ae
(i j : Fin 3)
{G : Foundation.Parabolic.Vec3 → ℝ}
(hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
{A : Set Foundation.Parabolic.Vec3}
(hA : MeasurableSet A)
:
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯
G =ᵐ[MeasureTheory.volume]
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯
(A.indicator G) + Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯
(Aᶜ.indicator G)
Splitting the source into two measurable spatial regions commutes with its concrete Riesz operator up to almost-everywhere equality.
theorem
CKN.Core.Step4.pressure_riesz_component_exterior_bound
(i j : Fin 3)
{δ : ℝ}
(hδ : 0 < δ)
{G : Foundation.Parabolic.Vec3 → ℝ}
(hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume)
(hGc : HasCompactSupport G)
{A U : Set Foundation.Parabolic.Vec3}
(hU : IsOpen U)
(hGA : ∀ y ∉ A, G y = 0)
(hAb : Bornology.IsBounded A)
(hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ ‖x - y‖)
:
∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict U, ‖Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ G x‖ₑ ≤ ENNReal.ofReal (4 * (4 * Real.pi)⁻¹ * (δ ^ 3)⁻¹) * ∫⁻ (y : Foundation.Parabolic.Vec3), ‖G y‖ₑ
On a region separated from the source, the concrete operator is bounded
by the spatial L^1 mass times the inverse cube of the separation.