Time integrability of the actual centered slice terms #
The sum of source norms and the real tensor energy in
eq:pressure-gradient-morrey are integrable on arbitrary interior time boxes.
Centered source control on arbitrary interior time boxes #
The source estimate in eq:pressure-gradient-morrey is valid on any local
box of def:sws, not only on a backward cylinder's time window.
theorem
CKN.Core.Step4.origin_centered_source_le_majorant_on_local_box
{Ω : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{q ρ : ℝ}
{x : Foundation.Parabolic.Vec3}
{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)
(hρ : 0 < ρ)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball x ρ) J)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∑ i : Fin 3,
MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) =>
pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff x hρ)
(spatialDeriv (mollifiedBallCutoff x hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s))
(fun (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, u (y, s) j) y i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ originCenteredSourceMajorant x ρ u Du s
The actual centered tensor source is bounded by the integrable source majorant on every interior ball-times-window box.
Measurability of the centered slice terms #
Spatial averaging and cutoff multiplication preserve product measurability
of the tensor and divergence source in eq:pressure-gradient-morrey.
theorem
CKN.Core.Step4.origin_velocity_average_aestronglyMeasurable
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => u w)
((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J)))
(j : Fin 3)
:
MeasureTheory.AEStronglyMeasurable (fun (s : ℝ) => ⨍ (y : Foundation.Parabolic.Vec3) in B, u (y, s) j)
(MeasureTheory.volume.restrict J)
Spatial component averages are measurable in time.
theorem
CKN.Core.Step4.origin_centered_source_product_aestronglyMeasurable
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{ρ : ℝ}
{J : Set ℝ}
(hρ : 0 < ρ)
(hu :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => u w)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)).prod (MeasureTheory.volume.restrict J)))
(hDu :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => Du w)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)).prod (MeasureTheory.volume.restrict J)))
(i : Fin 3)
:
MeasureTheory.AEStronglyMeasurable
(fun (w : Foundation.Parabolic.Vec3 × ℝ) =>
pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff x hρ) (spatialDeriv (mollifiedBallCutoff x hρ))
(fun (y : Foundation.Parabolic.Vec3) => u (y, w.2)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, w.2))
(fun (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, u (y, w.2) j) w.1 i)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))
The centered cutoff divergence source is jointly measurable on the full spatial space and the chosen time window.
theorem
CKN.Core.Step4.origin_tensor_energy_time_aemeasurable
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{ρ : ℝ}
{J : Set ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => u w)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)).prod (MeasureTheory.volume.restrict J)))
:
AEMeasurable
(fun (s : ℝ) =>
(∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, utensorNorm u x ρ s y ^ (3 / 2)) ^ (2 / 3))
(MeasureTheory.volume.restrict J)
The real tensor energy appearing in the harmonic bound is measurable in time.
noncomputable def
CKN.Core.Step4.originCenteredSourceNorm
(x : Foundation.Parabolic.Vec3)
{ρ : ℝ}
(hρ : 0 < ρ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(s : ℝ)
:
The sum of the three actual global centered-source norms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Core.Step4.origin_centered_source_norm_aemeasurable
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{ρ : ℝ}
{J : Set ℝ}
(hρ : 0 < ρ)
(hum :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => u w)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)).prod (MeasureTheory.volume.restrict J)))
(hdm :
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => Du w)
((MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x ρ)).prod (MeasureTheory.volume.restrict J)))
:
AEMeasurable (originCenteredSourceNorm x hρ u Du) (MeasureTheory.volume.restrict J)
Product measurability of velocity and gradient implies time measurability of the sum of the actual centered-source norms.
theorem
CKN.Core.Step4.origin_centered_source_norm_time_obligations
{Ω : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{q ρ : ℝ}
{x : Foundation.Parabolic.Vec3}
{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)
(hρ : 0 < ρ)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball x ρ) J)
:
AEMeasurable (originCenteredSourceNorm x hρ u Du) (MeasureTheory.volume.restrict J) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, originCenteredSourceNorm x hρ u Du s ≠ ⊤) ∧ MeasureTheory.Integrable (fun (s : ℝ) => (originCenteredSourceNorm x hρ u Du s).toReal)
(MeasureTheory.volume.restrict J)
The actual centered-source norm sum is measurable, finite a.e., and integrable in real value on every local ball-times-window box.
theorem
CKN.Core.Step4.origin_tensor_energy_integrable_on_local_box
{Ω : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{q ρ : ℝ}
{x : Foundation.Parabolic.Vec3}
{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)
(hρ : 0 < ρ)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball x ρ) J)
:
MeasureTheory.Integrable
(fun (s : ℝ) =>
(∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, utensorNorm u x ρ s y ^ (3 / 2)) ^ (2 / 3))
(MeasureTheory.volume.restrict J)
The real two-thirds power of the tensor energy is integrable on every interior ball-times-window box from suitability alone.