Numerical inputs for the origin pressure-gradient estimate #
The divergence-source norm and its clipped time-power coefficient, and the fixed-ball pressure and force time envelopes, are read off the data size and the velocity budgets. These are the numerical bounds a selected field is compared against.
Time growth of the divergence source on origin cells #
The component source in eq:pressure-gradient-morrey inherits the product
Morrey bound of velocity and its spatial gradient. Its spatial slice norms
then satisfy the clipped time growth in prop:bootstrap. This estimate is
for the uncentered divergence source; localization and subtraction of the
velocity average require additional terms.
theorem
CKN.Core.Step4.origin_divergence_source_clipped_time_bound
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{i : Fin 3}
{τ q κ R : ℝ}
{KU KD KF : ENNReal}
(hτ : 25 / 3 ≤ τ)
(hq : 5 / 2 < q)
(hκ : 6 / 5 ≤ κ)
(hκτ : κ ≤ (1 / τ + 8 / 25)⁻¹)
(hκq : κ ≤ q)
(hR : 0 < R)
(hRle : R ≤ 1)
(hU :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z j) ≤ KU)
(hD :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i j) ≤ KD)
(hF :
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) q
((Foundation.Parabolic.parabolicCylinder 0 0 R).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
f z i) ≤ KF)
(hUm :
∀ (j : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => u z j)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 R)))
(hDm :
∀ (j : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 R)))
(hFm :
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => f z i)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 R)))
(x : Foundation.Parabolic.Vec3)
(t : ℝ)
{r : ℝ}
(hr : 0 < r)
:
∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Du (y, s) i j * u (y, s) j - f (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R)) ^ (6 / 5) ≤ (3 * KU * KD + KF) ^ (6 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / κ)))
Integrating the uncentered source over a clipped origin cell preserves
its Morrey exponent and the explicit constant 3 KU KD + KF.
theorem
CKN.Core.Step4.origin_divergence_source_numerical_bounds_of_sws
(q τ R₀ R₁ ε : ℝ)
(KU KD : ENNReal)
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hR : 0 < R₁)
(hR₁₀ : R₁ ≤ R₀)
(hR₀le : R₀ ≤ 1)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{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)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hU :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i) ≤ KU)
(hD :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i j) ≤ KD)
(hsize :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε)
:
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q)
fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => ∑ j : Fin 3, Du w i j * u w j - f w i) z)) ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε) ∧ ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3) (t r : ℝ),
0 < r →
∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Du (y, s) i j * u (y, s) j - f (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ (3 * KU * KD + Endgame.forceSourceMorreyBound q ε) ^ (6 / 5) * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The suitable-solution data give the uncentered divergence-source norm and
its clipped time-power bound. The time coefficient is the 6/5 power of
the component norm bound. All numerical data precede the solution.