Pressure Gradient Source Morrey #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The source estimate on a spacetime carrier. The two product exponents
combine to (1 / τ + 8 / 25)⁻¹; the force is lowered from its q-Morrey
exponent only after the common target exponent has been selected.
theorem
CKN.Core.Step4.pressure_divergence_source_morrey_component_le
{S : Set Foundation.Parabolic.ParabolicPoint}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{i : Fin 3}
{τ q κ : ℝ}
{KU KD KF : ENNReal}
{z₀ : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hτ : 25 / 3 ≤ τ)
(hq : 5 / 2 < q)
(hκ : 6 / 5 ≤ κ)
(hκτ : κ ≤ (1 / τ + 8 / 25)⁻¹)
(hκq : κ ≤ q)
(hR : 0 < R)
(hRle : R ≤ 1)
(hSsupport : S ⊆ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R)
(hU :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) ≤ KU)
(hD :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD)
(hF :
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) q
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) ≤ KF)
(hUmeas :
∀ (j : Fin 3), AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) MeasureTheory.volume)
(hDmeas :
∀ (j : Fin 3),
AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume)
(hFmeas : AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) MeasureTheory.volume)
:
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, Du z i j * u z j - f z i) ≤ 3 * KU * KD + KF
theorem
CKN.Core.Step4.pressure_divergence_source_morrey_le
{S : Set Foundation.Parabolic.ParabolicPoint}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{τ q κ : ℝ}
{KU KD KF : ENNReal}
{z₀ : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hτ : 25 / 3 ≤ τ)
(hq : 5 / 2 < q)
(hκ : 6 / 5 ≤ κ)
(hκτ : κ ≤ (1 / τ + 8 / 25)⁻¹)
(hκq : κ ≤ q)
(hR : 0 < R)
(hRle : R ≤ 1)
(hSsupport : S ⊆ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R)
(hU :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) ≤ KU)
(hD :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD)
(hF :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) q
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) ≤ KF)
(hUmeas :
∀ (j : Fin 3), AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) MeasureTheory.volume)
(hDmeas :
∀ (i j : Fin 3),
AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume)
(hFmeas :
∀ (i : Fin 3), AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => f z i) MeasureTheory.volume)
:
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm
(S.indicator (fun (w : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => ∑ j : Fin 3, Du w i j * u w j - f w i)
z)) ≤ 3 * (3 * KU * KD + KF)