A temporal majorant for the fixed pressure remainder

The annular derivative estimate bounds the harmonic part by fixed energy and pressure slice norms. The far-force derivative is bounded by the spatial force integral. Their finite time moments follow from local suitability on one fixed cylinder, without a pressure oscillation estimate on smaller cells.

theorem CKN.Core.Step4.fixed_remainder_temporal_majorant_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} (hq : 5 / 2 < q) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∃ (M : ℝ → ENNReal), AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), ∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2), ‖classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) x i‖ₑ ≤ M s

Suitability gives a measurable finite 3/2 time majorant for every component of the gradient of the fixed harmonic and far-force remainder.