The bootstrap round of prop:bootstrap

The single round of cor:one-round, run with the cut-offs of Step 3 of the proof of thm:A. From the velocity in 𝓜^{3,25/3} and its gradient in 𝓜^{2,25/8} on the cylinder of radius 11/16, together with the pressure gradient in 𝓜^{6/5,25/11} on radius 43/64 supplied by lem:pressure-gradient-morrey, it returns the velocity in 𝓜^{3,25} on radius 5/8. The exponents are those of eq:bootstrap-gain: 1/ς = 1/τ - 2/25 with τ = 25/3; the undifferentiated source lies in 𝓜^{6/5,25/11} and the differentiated source in 𝓜^{3,25/6}.

Every source is split at t = 0 and only the past part is estimated, so no bound at times after 0 is used; the pressure values there enter only the local representation of the localized velocity.

theorem CKN.Core.Endgame.exists_uniform_bootstrap_of_initial_pressure (q ε₀ : ℝ) (KUinitial KD : ENNReal) (hq : 5 / 2 < q) (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 / 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) (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) : ∃ KU < ⊤, ∀ (Ω : 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 / 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) → ∫⁻ (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

The initial one-sided pressure-gradient estimate and literal localized equation give a solution-uniform improved velocity bound on the intermediate cylinder. Future-time pressure values enter only the local representation.