thm:endgame on the one-sided cylinder

The final step of the proof of thm:A. The velocity is taken in both 𝓜^{3,25} and 𝓜^{3,25/3} on the cylinder of radius 5/8, and the pressure gradient in 𝓜^{6/5,min {q, 25/9}} on radius 19/32, the exponent of eq:pressure-gradient-morrey at τ = 25 since 1/25 + 8/25 = 9/25. The localized sources are those of lem:local-equation, split at t = 0, and the heat-potential estimate of prop:heat-morrey-hoelder produces the Hölder representative on the closed half cylinder with exponent γ₀ = min {2 - 5/q, 1/5} of eq:gamma-value. Only local integrability of the pressure gradient, not a uniform bound at later times, is used to justify that representation.

theorem CKN.Core.Endgame.exists_uniform_halfCylinder_of_final_pressure (q ε₀ : ℝ) (KU KUinitial KD : ENNReal) (hq : 5 / 2 < q) (hε₀ : 0 ≤ ε₀) (hKU : KU < ⊤) (hKUinitial : KUinitial < ⊤) (hKD : KD < ⊤) (hGA : ∃ 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) (hL : ∀ (Ω : 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 → ∀ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ) (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), φ ∈ spaceTimeTestFunction Ω I → localBox Ω I U J → tsupport φ ⊆ U ×ˢ J → (∀ (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 ψ ⊆ U ×ˢ J → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) → 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) : ∃ (C₄ : ℝ), 0 ≤ C₄ ∧ ∀ (Ω : 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 → (∀ (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) → ∫⁻ (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 ε₀ → ∃ (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) C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z

The final local pressure-gradient estimate and the literal local heat representation yield a uniform closed-half-cylinder estimate, with the constant chosen before the domain and solution.