Morrey membership of a signed measurable pressure decomposition

Finite sums of the completed source fields and the measurable remainder control the same identified pressure field on its target carrier.

Morrey control of a windowed Riesz field

A completed-operator representative inherits the finite source Morrey seminorm once the bounded spatial support and the full-time slice membership are supplied by the fixed product restriction.

theorem CKN.Core.Step4.window_riesz_field_morrey_lt_top (j i : Fin 3) {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) {F T : Foundation.Parabolic.ParabolicPoint → ℝ} {x : Foundation.Parabolic.Vec3} {r : ℝ} (hr : 0 < r) {J : Set ℝ} (hJ : MeasurableSet J) (hF : AEMeasurable ((Foundation.Parabolic.vec3Ball x r ×ˢ J).indicator F) MeasureTheory.volume) (hFs : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hT : AEMeasurable T MeasureTheory.volume) (hident : ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => (Foundation.Parabolic.vec3Ball x r ×ˢ J).indicator F (y, s)) (hFnorm : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ ((Foundation.Parabolic.vec3Ball x r ×ˢ J).indicator F) < ⊤) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ T < ⊤

Product restriction supplies the bounded support and full-time slice membership needed to transfer a source Morrey bound to its Riesz field.

Morrey control from almost-everywhere remainder slice bounds

An almost-everywhere spatial bound is sufficient for the measurable remainder selected by weak derivative uniqueness. A bounded representative satisfies the pointwise consumer and preserves the original Morrey class.

theorem CKN.Core.Step4.pressure_remainder_indicator_morrey_lt_top_of_ae_slice_bound {κ : ℝ} (hκlo : 3 / 2 ≤ κ) (hκhi : κ ≤ 25 / 9) {H : Foundation.Parabolic.ParabolicPoint → ℝ} (hH : Measurable H) {M : ℝ → ENNReal} (hM : AEMeasurable M MeasureTheory.volume) {A : Set Foundation.Parabolic.ParabolicPoint} {B : Set Foundation.Parabolic.Vec3} (hA : MeasurableSet A) (hAB : ∀ w ∈ A, w.1 ∈ B) (hB : MeasurableSet B) (hBfinite : MeasureTheory.volume B < ⊤) (hbound : ∀ᵐ (s : ℝ) (x : Foundation.Parabolic.Vec3), (x, s) ∈ A → ‖H (x, s)‖ₑ ≤ M s) (hMfinite : ∫⁻ (s : ℝ), M s ^ (3 / 2) < ⊤) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ (A.indicator H) < ⊤

A finite temporal majorant controls the original measurable remainder in Morrey space even when the spatial bound initially holds only almost everywhere on each time slice.

theorem CKN.Core.Step4.ae_spatial_bound_on_product_of_restricted_slices {H : Foundation.Parabolic.ParabolicPoint → ℝ} {M : ℝ → ENNReal} {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hB : MeasurableSet B) (hJ : MeasurableSet J) (hbound : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖H (x, s)‖ₑ ≤ M s) : ∀ᵐ (s : ℝ) (x : Foundation.Parabolic.Vec3), (x, s) ∈ B ×ˢ J → ‖H (x, s)‖ₑ ≤ M s

A bound on a measurable product carrier, expressed with restricted space and time measures, has the full-time implication form needed by the remainder Morrey estimate.

theorem CKN.Core.Step4.finite_sum_morreyNorm_lt_top {ι : Type u_1} {P κ : ℝ} (hP : 1 ≤ P) (s : Finset ι) {F : ι → Foundation.Parabolic.ParabolicPoint → ℝ} (hF : ∀ j ∈ s, Measurable (F j)) (hN : ∀ j ∈ s, Foundation.Parabolic.Morrey.morreyNorm P κ (F j) < ⊤) : (Foundation.Parabolic.Morrey.morreyNorm P κ fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ j ∈ s, F j w) < ⊤

A finite sum of measurable scalar fields with finite Morrey seminorm again has finite Morrey seminorm.

theorem CKN.Core.Step4.morreyVecMem_of_signed_pressure_decomposition {κ : ℝ} (hκ : 6 / 5 ≤ κ) {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {T F : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} {H : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hT : ∀ (j i : Fin 3), Measurable (T j i)) (hF : ∀ (j i : Fin 3), Measurable (F j i)) (hH : ∀ (i : Fin 3), Measurable (H i)) (hTN : ∀ (j i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ (T j i) < ⊤) (hFN : ∀ (j i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ (F j i) < ⊤) (hHN : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ (S.indicator (H i)) < ⊤) (hid : ∀ (i : Fin 3), (fun (w : Foundation.Parabolic.ParabolicPoint) => Dp w i) =ᵐ[MeasureTheory.volume.restrict S] fun (w : Foundation.Parabolic.ParabolicPoint) => -∑ j : Fin 3, T j i w + H i w + ∑ j : Fin 3, F j i w) : morreyVecMem (6 / 5) κ S Dp

Finite source and remainder Morrey seminorms give the Morrey class of the same pressure field in the signed decomposition on a measurable carrier.