Time bounds for localized pressure sources

The spatial 6/5 norm on a cell has a finite 6/5 time moment from Morrey control. Intersecting the time window and spatial ball with carriers preserves the estimate, with the explicit radius power 5 * (1 - (6/5)/κ).

theorem CKN.Core.Step4.glued_clipped_slice_time_bound {F : Foundation.Parabolic.ParabolicPoint → ℝ} {κ : ℝ} (hF : AEMeasurable F MeasureTheory.volume) (B : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) : have W := Set.Ioc (z.2 - r ^ 2) z.2 ∩ J; have K := fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ B)); AEMeasurable K (MeasureTheory.volume.restrict W) ∧ ∫⁻ (t : ℝ) in W, K t ^ (6 / 5) ≤ ENNReal.ofReal r ^ (5 * (1 - 6 / 5 / κ)) * Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F ^ (6 / 5)

The clipped spatial slice norm obeys the exact Morrey radius growth.

theorem CKN.Core.Step4.glued_supported_source_slice_memLp {F : Foundation.Parabolic.ParabolicPoint → ℝ} {κ : ℝ} (hF : AEMeasurable F MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ F < ⊤) {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hs : ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, F w = 0) : ∀ᵐ (t : ℝ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

A bounded cylindrical source with finite Morrey norm has full-space 6/5 slices at almost every time.