Centred velocity Morrey data from suitable weak solutions

The mean correction is bounded in time and supported on a finite-measure space-time carrier. It therefore belongs to every finite integrability class needed here. Subtracting it preserves the velocity Morrey class.

Temporal bounds for the centring velocity

The local kinetic-energy essential supremum controls the spatial velocity mean. Thus centring the tensor introduces bounded temporal coefficients, not an additional assumption on the suitable solution.

theorem CKN.Core.Step4.pressure_source_mean_enorm_bound (v : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (B : Set Foundation.Parabolic.Vec3) (i : Fin 3) : ‖⨍ (y : Foundation.Parabolic.Vec3) in B, v y i‖ₑ ≤ ENNReal.ofReal (MeasureTheory.volume B).toReal⁻¹ * (MeasureTheory.volume B + ∫⁻ (y : Foundation.Parabolic.Vec3) in B, ‖v y‖ₑ ^ 2)

A component mean is bounded by the volume plus the kinetic energy, with the exact normalization factor of the spatial average.

theorem CKN.Core.Step4.pressure_source_mean_ae_bounded_of_sws {Ω : 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) {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I B J) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), |⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, s) i| ≤ C

Suitable weak solutions supply a finite temporal bound for each component of the mean on every relatively compact spatial box.

theorem CKN.Core.Step4.pressure_source_mean_aemeasurable_of_sws {Ω : 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) {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I B J) (i : Fin 3) : AEMeasurable (fun (s : ℝ) => ⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, s) i) (MeasureTheory.volume.restrict J)

The centring mean is measurable in time on each suitable-solution box.

theorem CKN.Core.Step4.pressure_source_morrey_lt_top_of_memLp {P κ : ℝ} (hP : 1 ≤ P) (hPκ : P ≤ κ) {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal κ) MeasureTheory.volume) : Foundation.Parabolic.Morrey.morreyNorm P κ g < ⊤

Global finite integrability at the outer exponent controls a Morrey seminorm with any smaller integrability exponent.

theorem CKN.Core.Step4.pressure_source_bounded_supported_morrey_lt_top {P κ C : ℝ} (hP : 1 ≤ P) (hPκ : P ≤ κ) {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (hSfinite : MeasureTheory.volume S < ⊤) {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hg : AEMeasurable g MeasureTheory.volume) (hbound : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), |g z| ≤ |C|) (hzero : ∀ z ∉ S, g z = 0) : Foundation.Parabolic.Morrey.morreyNorm P κ g < ⊤

A bounded measurable function on a finite-measure carrier has finite Morrey seminorm at each finite admissible pair of exponents.

theorem CKN.Core.Step4.pressure_centred_velocity_morrey_data_of_sws {τ : ℝ} (hτ : 3 ≤ τ) {Ω : 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) {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I B J) {S : Set Foundation.Parabolic.ParabolicPoint} (hS : MeasurableSet S) (hSbox : S ⊆ B ×ˢ J) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) < ⊤) (i : Fin 3) : AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i - ⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, z.2) i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i - ⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, z.2) i) < ⊤

The suitable-solution energy bound supplies the centred velocity Morrey data on every measurable subcarrier of a local box.