The first bootstrap's differentiated cutoff source #
The initial velocity exponent controls the actual differentiated source without lowering integrability. Unit-cylinder support then lowers only the outer Morrey exponent, with numerical factor one.
theorem
CKN.Core.Endgame.bootstrap_derivative_source_of_suitableWeakSolution
(C : ℝ)
(KU : ENNReal)
(hC : 0 ≤ C)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{φ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{u f : 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)
(hsupp :
∀ z ∈ tsupport φ,
z.2 ≤ 0 → Foundation.Parabolic.parabolicHomeomorph.symm z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16))
(hder : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), z.2 ≤ 0 → ∀ (j : Fin 3), |spatialPartial φ j z| ≤ C)
(hN :
∀ (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) ≤ KU)
(j i : Fin 3)
:
AEMeasurable (causalDerivativeComponent φ u j i) MeasureTheory.volume ∧ Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) (causalDerivativeComponent φ u j i) ≤ ENNReal.ofReal (2 * C) * KU
The literal differentiated source has the first-bootstrap exponents and an explicit bound from the initial velocity and cutoff derivatives.