Parabolic Morrey bounds for the spatial pressure Riesz operator

For a spatially supported source, finitely many annuli suffice at every cell. The normalized bound is uniform in their number. It therefore bounds the Morrey seminorm of any measurable representative of the slice operator.

noncomputable def CKN.Core.Step4.pressureRieszMorreyConstant (κ : ℝ) : ENNReal

The explicit constant in the parabolic Morrey bound for one spatial Riesz component.

Equations

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

theorem CKN.Core.Step4.pressureRieszMorreyConstant_lt_top (κ : ℝ) : pressureRieszMorreyConstant κ < ⊤

The explicit component constant is finite.

theorem CKN.Core.Step4.pressure_riesz_normalized_slice_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) {L : ℝ} (hsupport : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), L < ‖y‖ → F (y, s) = 0) (x : Foundation.Parabolic.Vec3) (t : ℝ) {r : ℝ} (hr : 0 < r) : 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) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ^ (6 / 5)) ^ (5 / 6) ≤ pressureRieszMorreyConstant κ * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F

The canonical slice operator has the normalized time bound itself; no choice of a jointly measurable representative is needed for this form.

theorem CKN.Core.Step4.pressure_riesz_morreyNorm_bound (i j : Fin 3) {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) {F T : 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) {L : ℝ} (hsupport : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), L < ‖y‖ → F (y, s) = 0) (hT : AEMeasurable T MeasureTheory.volume) (hident : ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ T ≤ pressureRieszMorreyConstant κ * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F

The concrete spatial Riesz operator preserves the parabolic Morrey seminorm in the pressure-gradient range, for a measurable representative of its slice action and a spatially supported source.

theorem CKN.Core.Step4.pressure_riesz_morreyNorm_lt_top (i j : Fin 3) {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) {F T : 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) {L : ℝ} (hsupport : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), L < ‖y‖ → F (y, s) = 0) (hT : AEMeasurable T MeasureTheory.volume) (hident : ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (hFnorm : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F < ⊤) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ T < ⊤

Finite source Morrey seminorm gives finite Morrey seminorm of its measurable concrete Riesz representative.

theorem CKN.Core.Step4.pressure_riesz_restricted_morreyNorm_bound (i j : Fin 3) {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) {F T : 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) {L : ℝ} (hsupport : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), L < ‖y‖ → F (y, s) = 0) {B : Set Foundation.Parabolic.Vec3} (hB : MeasurableSet B) (hT : AEMeasurable T MeasureTheory.volume) (hTzero : ∀ (y : Foundation.Parabolic.Vec3) (s : ℝ), y ∉ B → T (y, s) = 0) (hident : ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume.restrict B] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input i j) ⋯ fun (y : Foundation.Parabolic.Vec3) => F (y, s)) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ T ≤ pressureRieszMorreyConstant κ * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F

Restriction to a measurable spatial carrier preserves the concrete Riesz bound when the selected representative agrees with the operator only on that carrier and is zero outside it.