Source Morrey Gradient Instances #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.Endgame.first_round_source_package_of_step2
(q ε₀ C : ℝ)
(KU KD KP : ENNReal)
(hq : 5 / 2 < q)
(hC : 0 ≤ C)
(hKU : KU < ⊤)
(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 (11 / 16))
(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 / 3)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU)
(hD :
∀ (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)
(hDp :
∀ (i : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Dp z i)
MeasureTheory.volume)
(hP :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11)
((Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16)).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 ε₀)
:
have F := fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => causalGradientSourceComponent φ u Du f Dp i z;
have H := fun (j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => -causalDerivativeComponent φ u j i z;
(∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => F z i) MeasureTheory.volume) ∧ (∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) MeasureTheory.volume) ∧ (∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) =>
F z i) ≤ bootstrapGradientMorreyBound q ε₀ C KU KD KP) ∧ (∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) => H j z i) ≤ ENNReal.ofReal (2 * C) * KU) ∧ (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (F z)) < ⊤ ∧ (∀ (j : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (H j z)) < ⊤) ∧ (∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16), F z = 0) ∧ ∀ (j : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 (11 / 16), H j z = 0
The quantitative first-round source data in the exact slots used by the bootstrap consumer. The derivative slot carries the Duhamel sign.