Pressure oscillation on clipped origin windows

The pressure contribution to the slice bound is controlled by its spatial 3/2 power mass and Hölder in time. The required mass exponent is 13/2 - 15/(2κ), which yields the gradient mass exponent 5 - 6/κ. The separate large-radius estimate is supplied by pressure_gradient_origin_cylinder_large_cell_le in PressureGradientLargeCells. No estimate for the complete slice majorant is asserted here.

theorem CKN.Core.Step4.originClause_pressure_clipped_holder {P : Foundation.Parabolic.ParabolicPoint → ℝ} {x : Foundation.Parabolic.Vec3} {t r R : ℝ} (hr : 0 < r) (hm : MeasureTheory.AEStronglyMeasurable P ((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (2 * r))).prod (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0)))) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, (ENNReal.ofReal ((2 * r) ^ (-1 / 2)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => P (y, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (2 * r)))) ^ (6 / 5) ≤ ENNReal.ofReal ((2 * r) ^ (-3 / 5)) * ((∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * r), ‖P (y, s)‖ₑ ^ (3 / 2)) ^ (4 / 5) * ENNReal.ofReal (r ^ 2) ^ (1 / 5))

Hölder in a clipped time window for the pressure part of the doubled slice estimate, retaining its spatial power mass on that same window.

theorem CKN.Core.Step4.originClause_pressure_clipped_growth {P : Foundation.Parabolic.ParabolicPoint → ℝ} {x : Foundation.Parabolic.Vec3} {t r R κ : ℝ} {K : ENNReal} (hr : 0 < r) (hm : MeasureTheory.AEStronglyMeasurable P ((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (2 * r))).prod (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0)))) (hpressure : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * r), ‖P (y, s)‖ₑ ^ (3 / 2) ≤ K * ENNReal.ofReal (r ^ (13 / 2 - 15 / (2 * κ)))) : ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, (ENNReal.ofReal ((2 * r) ^ (-1 / 2)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => P (y, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x (2 * r)))) ^ (6 / 5) ≤ ENNReal.ofReal (2 ^ (-3 / 5)) * K ^ (4 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

The precise pressure mass exponent gives the growth exponent used for L^{6/5} gradients, without a loss from time clipping.

theorem CKN.Core.Step4.originClauseGauge_pressure_growth_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₁ κ : ℝ} {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} (Kp : ENNReal) (hKp : Kp < ⊤) (hpressure : ∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (r : ℝ), 0 < r → r ≤ (1 - R₁) / 4 → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 (2 * r), ‖p (y, s) - ⨍ (v : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 R₁, p (v, s)‖ₑ ^ (3 / 2) ≤ Kp * ENNReal.ofReal (r ^ (13 / 2 - 15 / (2 * κ)))) (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁one : R₁ < 1) : have A := ENNReal.ofReal (2 ^ (-3 / 5)) * Kp ^ (4 / 5); A < ⊤ ∧ ∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (r : ℝ), 0 < r → r ≤ (1 - R₁) / 4 → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, (ENNReal.ofReal ((2 * r) ^ (-1 / 2)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => p (y, s) - ⨍ (v : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball 0 R₁, p (v, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 (2 * r)))) ^ (6 / 5) ≤ A * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))

A single explicit pressure oscillation hypothesis gives the pressure contribution's growth on every margin-small cell centred in the closed carrier. The spatial mean is the same fixed carrier mean as in originClauseGaugeMajorant. Measurability of that mean and of the local pressure slices follows from suitability.