Quantitative majorant for the centred source on a slice ball

This module controls the absolute spatial mean of one slice component by the slice L³ norm, and splits the centred source majorant of eq:pressure-gradient-decomposition into a mixed velocity-gradient term, a quadratic velocity term, and a localized force term, with explicit numerical constants.

theorem CKN.Core.Step4.ofReal_ball_average_abs_mul_rpow_le_eLpNorm {x : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ))) : ENNReal.ofReal (⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, |g y|) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x ρ) ^ (1 / 3) ≤ MeasureTheory.eLpNorm g 3 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ))

The absolute spatial mean of one component is controlled by the slice L³ norm.

theorem CKN.Core.Step4.centredSWSCentredMajorant_le_three_terms {x : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (q : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) (hu : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ))) : centredSWSCentredMajorant x ρ q u Du f s ≤ 18 * (MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 3 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ))) + 18 * ENNReal.ofReal (cutoffGradientConstant / ρ) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x ρ) ^ (1 / 6) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 3 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)) ^ 2 + 4 * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x ρ) ^ (5 / 6 - 1 / q) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (ENNReal.ofReal q) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ))

The centred source majorant splits into a mixed term, a quadratic velocity term and a force term, with explicit numerical coefficients.