Initial Morrey estimates on a larger interior cylinder #
The initial velocity, pressure, and gradient estimates extend by zero from the cylinder of radius eleven sixteenths. The numerical bounds agree with the smaller-cylinder estimates; the gradient covering number is selected before the domain and solution.
theorem
CKN.Core.Endgame.wide_velocity_morrey_of_decay
(M r₀ ε₀ : ℝ)
(hM : 0 ≤ M)
(hr₀ : 0 < r₀)
(hrquarter : r₀ ≤ 1 / 4)
{Ω : 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)
(hQ₁ : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hdata :
∫⁻ (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 ε₀)
(hdec :
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ), 0 < r → r ≤ r₀ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
(i : Fin 3)
:
Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i) ≤ oneSidedVelocityMorreyBound M r₀ ε₀
Uniform scalar velocity Morrey control follows from one-sided decay and the original unit-cylinder smallness hypothesis.
theorem
CKN.Core.Endgame.wide_pressure_morrey_of_decay
(M r₀ ε₀ : ℝ)
(hM : 0 ≤ M)
(hr₀ : 0 < r₀)
(hrquarter : r₀ ≤ 1 / 4)
{Ω : 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)
(hQ₁ : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hdata :
∫⁻ (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 ε₀)
(hdec :
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ), 0 < r → r ≤ r₀ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
:
Foundation.Parabolic.Morrey.morreyNorm (3 / 2) (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator p) ≤ oneSidedPressureMorreyBound M r₀ ε₀
Uniform pressure Morrey control follows from one-sided decay and the original unit-cylinder smallness hypothesis.
theorem
CKN.Core.Endgame.wide_gradient_morrey_of_decay
(M r₀ : ℝ)
(hM : 0 ≤ M)
(hr₀ : 0 < r₀)
(hrquarter : r₀ ≤ 1 / 4)
:
∃ (N : ℕ),
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ), 0 < r → r ≤ r₀ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5)) →
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ oneSidedGradientMorreyBound M r₀ N
Uniform decay gives a quantitative gradient Morrey bound. The covering number is chosen before all domains and solutions.
theorem
CKN.Core.Endgame.wide_initial_morrey_of_decay
(M r₀ ε₀ : ℝ)
(hM : 0 ≤ M)
(hr₀ : 0 < r₀)
(hrquarter : r₀ ≤ 1 / 4)
:
∃ (N : ℕ),
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
∫⁻ (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 ε₀ →
(∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ), 0 < r → r ≤ r₀ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5)) →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ oneSidedVelocityMorreyBound M r₀ ε₀) ∧ (∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ oneSidedGradientMorreyBound M r₀ N) ∧ Foundation.Parabolic.Morrey.morreyNorm (3 / 2) (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator p) ≤ oneSidedPressureMorreyBound M r₀ ε₀
The three initial Morrey estimates on the larger interior cylinder have uniform numerical bounds and a covering number independent of the solution.