Source Morrey Slice #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The slicewise interface for the divergence-form pressure source carrying a spatial cutoff. These bounds are source estimates only; they do not select a weak pressure gradient or prove its spacetime pairing.
def
CKN.Core.Step4.sourceMorreyCutoffV
(η : Foundation.Parabolic.Vec3 → ℝ)
(dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ)
(u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3)
(f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
:
Cutoff pressure-Poisson source used to estimate the selected gradient in Morrey spaces.
Equations
- CKN.Core.Step4.sourceMorreyCutoffV η dη u Du f = CKN.Core.Step4.pressureDivergenceCutoffSource η dη u Du f
Instances For
theorem
CKN.Core.Step4.sourceMorreyCutoffV_slice_bound
{B : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{q Cη Cdη : ℝ}
{KU KD KF : ENNReal}
(hq : 5 / 2 < q)
(hμ : (MeasureTheory.volume.restrict B) Set.univ < ⊤)
(hCη : 0 ≤ Cη)
(hCdη : 0 ≤ Cdη)
(hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B))
(hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |η x| ≤ Cη)
(hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B))
(hdηbound : ∀ (j : Fin 3), ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, |dη j x| ≤ Cdη)
(hU :
∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x j) (ENNReal.ofReal 3)
(MeasureTheory.volume.restrict B) ≤ KU)
(hD :
∀ (i j : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (ENNReal.ofReal 2)
(MeasureTheory.volume.restrict B) ≤ KD)
(hF :
∀ (i : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f x i) (ENNReal.ofReal q)
(MeasureTheory.volume.restrict B) ≤ KF)
(hUmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x j) (MeasureTheory.volume.restrict B))
(hDmeas :
∀ (i j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j)
(MeasureTheory.volume.restrict B))
(hFmeas :
∀ (i : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => f x i) (MeasureTheory.volume.restrict B))
:
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffV η dη u Du f x)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ 3 * (3 * (ENNReal.ofReal Cη * KD * KU + ENNReal.ofReal Cdη * (KU * KU * (MeasureTheory.volume.restrict B) Set.univ ^ (1 / 6))) + ENNReal.ofReal Cη * (KF * (MeasureTheory.volume.restrict B) Set.univ ^ (5 / 6 - 1 / q)))