Time integration of spatial source masses

Spatial Hölder converts the L^1 mass of a source on a ball into its L^{6/5} mass. Enlarging the time window to the ball's parabolic scale then makes the source's Morrey bound available for exterior kernel terms.

theorem CKN.Core.Step4.pressure_source_spatial_mass_power_bound {G : Foundation.Parabolic.Vec3 → ℝ} {B : Set Foundation.Parabolic.Vec3} (hG : AEMeasurable G (MeasureTheory.volume.restrict B)) : (∫⁻ (y : Foundation.Parabolic.Vec3) in B, ‖G y‖ₑ) ^ (6 / 5) ≤ MeasureTheory.volume B ^ (1 / 5) * ∫⁻ (y : Foundation.Parabolic.Vec3) in B, ‖G y‖ₑ ^ (6 / 5)

Spatial Hölder, raised to the source exponent, retains the ball's volume to the power 1/5.

theorem CKN.Core.Step4.pressure_source_spatial_mass_time_power_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) {x : Foundation.Parabolic.Vec3} {t r ρ : ℝ} (hr : 0 < r) (hrρ : r ≤ ρ) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, (∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, ‖F (y, s)‖ₑ) ^ (6 / 5) ≤ MeasureTheory.volume (Foundation.Parabolic.vec3Ball x ρ) ^ (1 / 5) * Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) F (x, t) ρ

A smaller cell time window is controlled by the full parabolic cylinder at the source ball's radius.

theorem CKN.Core.Step4.pressure_source_exterior_mass_time_bound {κ : ℝ} {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) {x : Foundation.Parabolic.Vec3} {t r ρ : ℝ} (hr : 0 < r) (hrρ : r ≤ ρ) : ENNReal.ofReal ρ ^ (-3) * (∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, (∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, ‖F (y, s)‖ₑ) ^ (6 / 5)) ^ (5 / 6) ≤ ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 6) * ENNReal.ofReal ρ ^ (5 / 3 - 5 / κ) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F

The inverse-cube exterior kernel factor converts the integrated source mass into the Morrey tail power ρ^{5/3 - 5/κ}.

theorem CKN.Core.Step4.pressure_source_slice_norm_aemeasurable {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (B : Set Foundation.Parabolic.Vec3) : AEMeasurable (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B)) MeasureTheory.volume

The spatial slice norm agrees almost everywhere with its integral formula, and is measurable as a function of time.

theorem CKN.Core.Step4.pressure_source_slice_norm_time_power_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) {x : Foundation.Parabolic.Vec3} {t r ρ : ℝ} (hr : 0 < r) (hrρ : r ≤ ρ) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => F (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)) ^ (6 / 5) ≤ Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) F (x, t) ρ

The time integral of a spatial slice norm over a cell window is controlled by the source power integral on a larger cylinder.

theorem CKN.Core.Step4.pressure_source_cylinder_power_root_bound {κ : ℝ} (F : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {ρ : ℝ} (hρ : 0 < ρ) : Foundation.Parabolic.Morrey.cylinderPowerIntegral (6 / 5) F z ρ ^ (5 / 6) ≤ ENNReal.ofReal ρ ^ (25 / 6 - 5 / κ) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F

Removing the Morrey normalization recovers the source's cell mass with its exact positive radius power.