The one-sided pressure-gradient boundary in its three consumed shapes #
The small-data theorem thm:A of paper/ckn.tex uses the one-sided
pressure-gradient estimate of prop:bootstrap in three different spellings.
The estimate itself is recorded by oneSidedPressureGradientQuantitative,
whose majorant is the explicit formula oneSidedPressureGradientKP. The
small-data statement instead asks only for some finite majorant, uniformly
in the velocity exponent τ ∈ [25/3, 25] and in the two radii. The uniform
bootstrap round and the closed half-cylinder estimate ask for the two
numerical instantiations (τ, R₀, R₁) = (25/3, 11/16, 43/64) and
(25, 5/8, 19/32), with the solution fields explicit, the hypotheses in the
order hsol → hdom → hsmall → hU → hD, and the measurability carrier written
as spaceTimeSet (vec3Ball 0 R₁) I.
The three theorems below are the translations between those spellings. The
exponent normalizations are exact: at τ = 25/3 the Morrey exponent
min ((1/τ + 8/25)⁻¹) q equals 25/11, because 25/11 < 5/2 < q, while at
τ = 25 it equals min q (25/9) and the minimum genuinely survives, since
q is only known to exceed 5/2 = 22.5/9. Nothing in this translation is
special to either numerical instantiation: the majorant formula, its
finiteness, and the estimate are all uniform in τ.
The hypothesis named hGA throughout the assembly of thm:A is
lem:pressure-gradient-morrey. These theorems only rewrite it between
spellings: existential majorant against explicit majorant, free centre
against origin carrier, and the two orders in which the solution hypotheses
are presented. No estimate is strengthened or weakened here.
theorem
CKN.Core.Endgame.pressure_gradient_existential_of_quantitative
(hGA : Step4.oneSidedPressureGradientQuantitative)
(q τ C_CZ R₀ R₁ ε : ℝ)
(KU KD : ENNReal)
:
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∃ KP < ⊤,
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ →
∀ (i : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP
The explicit majorant of prop:bootstrap witnesses the existential
majorant that the small-data statement asks for, at every admissible velocity
exponent and radius pair. No numerical instantiation is involved.
theorem
CKN.Core.Endgame.initial_pressure_output_of_existential
(hGA :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∃ KP < ⊤,
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ →
∀ (i : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5)
(min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP)
(q C_CZ ε₀ : ℝ)
(KUinitial KD : ENNReal)
(hq : 5 / 2 < q)
(hC : 0 ≤ C_CZ)
(hε₀ : 0 ≤ ε₀)
(hKUinitial : KUinitial < ⊤)
(hKD : KD < ⊤)
:
∃ KP < ⊤,
∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ),
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 ε₀ →
(∀ (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) ≤ KUinitial) →
(∀ (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) ≤ KD) →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 (43 / 64)) I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 (43 / 64) →
∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 (43 / 64) ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11)
((Foundation.Parabolic.parabolicCylinder 0 0 (43 / 64)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP
The existential form at (τ, R₀, R₁) = (25/3, 11/16, 43/64), in the exact
shape the uniform bootstrap round consumes: explicit solution fields, the
hypothesis order hsol → hdom → hsmall → hU → hD, the measurability carrier
written as a space-time set, and the Morrey exponent already normalized to
25/11.
theorem
CKN.Core.Endgame.final_pressure_output_of_existential
(hGA :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∃ KP < ⊤,
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ →
∀ (i : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5)
(min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP)
(q C_CZ ε₀ : ℝ)
(KU KD : ENNReal)
(hq : 5 / 2 < q)
(hC : 0 ≤ C_CZ)
(hε₀ : 0 ≤ ε₀)
(hKU : KU < ⊤)
(hKD : KD < ⊤)
:
∃ KP < ⊤,
∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(p : Foundation.Parabolic.ParabolicPoint → ℝ),
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 ε₀ →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 25
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 (19 / 32)) I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 (19 / 32) →
∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 (19 / 32) ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
((Foundation.Parabolic.parabolicCylinder 0 0 (19 / 32)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ KP
The existential form at (τ, R₀, R₁) = (25, 5/8, 19/32), in the exact
shape the closed half-cylinder estimate consumes. Here the Morrey exponent
stays a minimum: q is only known to exceed 5/2, so min q (25/9) cannot
be simplified further.