Uniform Morrey bounds for spatially bounded remainders #
Finite spatial support controls large cells, while the spatial volume of a
cell controls small cells. Together these estimates give a finite Morrey
seminorm from an L^{3/2} temporal bound on the spatial supremum.
theorem
CKN.Core.Step4.pressure_remainder_supported_cylinder_power_bound
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{H : ℝ → ENNReal}
{S : Set Foundation.Parabolic.Vec3}
(hF : AEMeasurable F MeasureTheory.volume)
(hH : AEMeasurable H MeasureTheory.volume)
(hS : MeasurableSet S)
(hsupport : ∀ x ∉ S, ∀ (t : ℝ), F (x, t) = 0)
(hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s)
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hr : 0 < r)
:
Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) F (x, t) r ≤ MeasureTheory.volume S * (∫⁻ (s : ℝ), H s ^ (3 / 2)) ^ (4 / 5) * ENNReal.ofReal r ^ (2 / 5)
Finite spatial support replaces the cell's spatial volume in the power-integral estimate.
theorem
CKN.Core.Step4.pressure_remainder_supported_morreyCell_bound
{κ : ℝ}
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{H : ℝ → ENNReal}
{S : Set Foundation.Parabolic.Vec3}
(hF : AEMeasurable F MeasureTheory.volume)
(hH : AEMeasurable H MeasureTheory.volume)
(hS : MeasurableSet S)
(hsupport : ∀ x ∉ S, ∀ (t : ℝ), F (x, t) = 0)
(hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
:
Foundation.Parabolic.Morrey.morreyCell (6 / 5) κ F z r ≤ MeasureTheory.volume S ^ (5 / 6) * (∫⁻ (s : ℝ), H s ^ (3 / 2)) ^ (2 / 3) * ENNReal.ofReal r ^ (5 / κ - 23 / 6)
The supported estimate after normalization, useful for cells of radius at least one.
theorem
CKN.Core.Step4.pressure_remainder_morreyNorm_bound
{κ : ℝ}
(hκlo : 3 / 2 ≤ κ)
(hκhi : κ ≤ 25 / 9)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{H : ℝ → ENNReal}
{S : Set Foundation.Parabolic.Vec3}
(hF : AEMeasurable F MeasureTheory.volume)
(hH : AEMeasurable H MeasureTheory.volume)
(hS : MeasurableSet S)
(hsupport : ∀ x ∉ S, ∀ (t : ℝ), F (x, t) = 0)
(hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s)
:
All cell radii are controlled by a single explicit constant.
theorem
CKN.Core.Step4.pressure_remainder_morreyNorm_lt_top
{κ : ℝ}
(hκlo : 3 / 2 ≤ κ)
(hκhi : κ ≤ 25 / 9)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{H : ℝ → ENNReal}
{S : Set Foundation.Parabolic.Vec3}
(hF : AEMeasurable F MeasureTheory.volume)
(hH : AEMeasurable H MeasureTheory.volume)
(hS : MeasurableSet S)
(hSfinite : MeasureTheory.volume S < ⊤)
(hsupport : ∀ x ∉ S, ∀ (t : ℝ), F (x, t) = 0)
(hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), ‖F (x, s)‖ₑ ≤ H s)
(hHfinite : ∫⁻ (s : ℝ), H s ^ (3 / 2) < ⊤)
:
The spatially supported remainder has finite Morrey seminorm whenever
its temporal supremum belongs to L^{3/2}.
theorem
CKN.Core.Step4.pressure_remainder_indicator_morreyNorm_lt_top
{κ : ℝ}
(hκlo : 3 / 2 ≤ κ)
(hκhi : κ ≤ 25 / 9)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
{H : ℝ → ENNReal}
{A : Set Foundation.Parabolic.ParabolicPoint}
{S : Set Foundation.Parabolic.Vec3}
(hA : MeasurableSet A)
(hAS : ∀ z ∈ A, z.1 ∈ S)
(hF : AEMeasurable F (MeasureTheory.volume.restrict A))
(hH : AEMeasurable H MeasureTheory.volume)
(hS : MeasurableSet S)
(hSfinite : MeasureTheory.volume S < ⊤)
(hbound : ∀ᵐ (s : ℝ), ∀ (x : Foundation.Parabolic.Vec3), (x, s) ∈ A → ‖F (x, s)‖ₑ ≤ H s)
(hHfinite : ∫⁻ (s : ℝ), H s ^ (3 / 2) < ⊤)
:
A measurable restriction to a finite spatial carrier has finite Morrey seminorm under a temporal bound on its spatial supremum.