Quantitative bounds for the centred source

The slice norms in def:sws give the uncentred source estimate, the mean-component bounds, and the localized force estimate used in eq:pressure-gradient-decomposition. All coefficients are explicit and independent of the solution.

noncomputable def CKN.Core.Step4.centredSWSUncentredMajorant (x : Foundation.Parabolic.Vec3) (ρ 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 : ℝ) : ENNReal

The uncentred source majorant in eq:pressure-gradient-decomposition, using the native vector norms of the velocity, gradient, and force slices.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.centredSWS_uncentred_bound_ae {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffV (mollifiedBallCutoff z.1 hρ) (spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) x) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffV (mollifiedBallCutoff z.1 hρ) (spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) x) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ centredSWSUncentredMajorant z.1 ρ q u Du f s

The uncentred estimate of eq:pressure-gradient-decomposition follows from suitable solution data, with the explicit constants 3, 1, and the cutoff derivative bound.

theorem CKN.Core.Step4.centredSWS_low_exponent_bounds_ae {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (j : Fin 3), ‖sourceSliceCentredMean z.1 ρ u s j‖ ≤ ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, |u (y, s) j|) ∧ (∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 3 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball z.1 ρ) ^ (1 / 2)) ∧ ∀ (i j : Fin 3), MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) i j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball z.1 ρ) ^ (1 / 3)

Finite-volume Hölder bounds for the low-exponent velocity and gradient components used in the mean correction of eq:pressure-gradient-decomposition.

theorem CKN.Core.Step4.centredSWS_force_bound_ae {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), MeasureTheory.MemLp (fun (y : Vec 3) => mollifiedBallCutoff z.1 hρ y * f (y, s) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (y : Vec 3) => mollifiedBallCutoff z.1 hρ y * f (y, s) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (ENNReal.ofReal q) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball z.1 ρ) ^ (5 / 6 - 1 / q)

The localized force in eq:pk has global L^{6/5} membership and its explicit finite-volume Hölder bound on almost every suitable-solution slice.