The fixed final cutoff and the quantitative half-cylinder conclusion #
The derivative constant is chosen before the domain. Pressure estimates on the radius-19/32 cylinder suffice, by a past-time extension which leaves the literal localized source unchanged. The remaining input is exactly the global heat representation of the localized velocity.
Quantitative consumption of the literal localized sources #
The actual gradient-slot and derivative-slot source estimates imply the closed-half-cylinder Hölder conclusion once their literal heat representation is supplied. This consumer does not construct that representation or the pressure gradient. All norm estimates concern only nonpositive times.
The numerical derivative-source coefficient from the initial velocity Morrey bound and the cutoff derivative bound.
Equations
- CKN.Core.Endgame.causalDerivativeMorreyBound C KUinitial = ENNReal.ofReal (2 * C) * (MeasureTheory.volume (CKN.Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / 3) * KUinitial)
Instances For
theorem
CKN.Core.Endgame.causalDerivativeMorreyBound_lt_top
(C : ℝ)
{KUinitial : ENNReal}
(hKUinitial : KUinitial < ⊤)
:
Finite initial velocity bounds give a finite derivative-source bound.
theorem
CKN.Core.Endgame.uniform_halfCylinder_of_literal_causal_sources
(q ε₀ C : ℝ)
(KU KUinitial KD KP : ENNReal)
(hq : 5 / 2 < q)
(hε₀ : 0 ≤ ε₀)
(hC : 0 ≤ C)
(hKU : KU < ⊤)
(hKUinitial : KUinitial < ⊤)
(hKD : KD < ⊤)
(hKP : KP < ⊤)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{u f Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hφ : φ ∈ spaceTimeTestFunction Ω I)
(hφrange : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ φ z ∧ φ z ≤ 1)
(hsupp :
∀ z ∈ tsupport φ,
z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8))
(hder :
∀ (z : Foundation.Parabolic.Vec3 × ℝ),
z.2 ≤ 0 →
|timePartial φ z| ≤ C ∧ (∀ (j : Fin 3), |spatialPartial φ j z| ≤ C) ∧ |spatialLaplacian (fun (x : Foundation.Parabolic.Vec3) => φ (x, z.2)) z.1| ≤ C)
(hU :
∀ (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)
(hUinitial :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i) ≤ KUinitial)
(hD :
∀ (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)
(hDp :
∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Dp z i)
MeasureTheory.volume)
(hP :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Dp z i) ≤ KP)
(hsmall :
∫⁻ (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 ε₀)
(hrep :
u =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential
(fun (w : Foundation.Parabolic.ParabolicPoint) => Step4.localizedGradientSourceG φ u Du f Dp w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => Step4.localizedGradientSourceH φ u j w i) z)
:
∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w (stepGamma₀ q)
(uniformHalfCylinderHolderBound q ε₀ (causalGradientMorreyBound q ε₀ C KU KD KP)
(causalDerivativeMorreyBound C KUinitial)) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z
Actual source estimates consume a literal localized heat representation to give a uniform closed-half-cylinder representative and interior regularity. The source and pressure-gradient bounds remain explicit hypotheses.
theorem
CKN.Core.Endgame.exists_uniform_final_cutoff_consumer :
∃ (C : ℝ),
0 < C ∧ ∀ (q ε₀ : ℝ) (KU KUinitial KD KP : ENNReal),
5 / 2 < q →
0 ≤ ε₀ →
KU < ⊤ →
KUinitial < ⊤ →
KD < ⊤ →
KP < ⊤ →
∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(u f Dp : 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 →
(∀ (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 : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (5 / 8)).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 (5 / 8)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
(∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (19 / 32)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
MeasureTheory.volume) →
(∀ (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) →
∫⁻ (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.Vec3 × ℝ → ℝ) (Ω' : Set Foundation.Parabolic.Vec3)
(J : Set ℝ),
φ ∈ spaceTimeTestFunction Ω I →
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
(∀ z ∈ tsupport φ, z.1 ∈ Foundation.Parabolic.vec3Ball 0 (9 / 16)) →
(∀ z ∈ tsupport φ,
z.2 ≤ 0 →
Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (9 / 16)) →
Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j w i)
z) →
∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
u ∧ ParabolicHolderVecNormLE
(closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w
(stepGamma₀ q)
(uniformHalfCylinderHolderBound q ε₀
(causalGradientMorreyBound q ε₀ C KU KD KP)
(causalDerivativeMorreyBound C KUinitial)) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0,
IsRegularPoint Ω I u z
A domain-independent final cutoff constant gives the quantitative half-cylinder conclusion from component bounds and literal localized heat representations. No global pressure-gradient estimate is needed.