Slice Selected Gradient Centred Source

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The centred divergence-form source for the selected pressure gradient

The source below is the one paired with the singly centred tensor pressureUTensor u c. The constant vector c is spatially constant. A force term remains in the source, so its tested identity has an additional force pairing unless that pairing is separately known to vanish.

The elementary reason for using the centred source is recorded here as a compiled pointwise probe: with u ≡ a, Du = 0, f = 0, and c = 0, the uncentred source is zero while the centred tensor has a nonzero (0,0) entry.

def CKN.Core.Step4.pressureDivergenceCutoffSourceCentred (η : 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) (c : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

The centred divergence-form source paired with pressureUTensor u c.

Equations

• CKN.Core.Step4.pressureDivergenceCutoffSourceCentred η dη u Du f c x i = ∑ j : Fin 3, (η x * Du x i j * (u x j - c j) + dη j x * u x i * (u x j - c j)) - η x * f x i

def CKN.Core.Step4.sourceMorreyCutoffVCentred (η : 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) (c : Foundation.Parabolic.Vec3) : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3

Alias used by the source-Morrey and slice-selection interfaces.

Equations

• CKN.Core.Step4.sourceMorreyCutoffVCentred η dη u Du f c = CKN.Core.Step4.pressureDivergenceCutoffSourceCentred η dη u Du f c

theorem CKN.Core.Step4.sourceMorreyCutoffVCentred_slice_bound_of_uncentred {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} {c : Foundation.Parabolic.Vec3} {i : Fin 3} {Cη Cdη Cc : ℝ} {KU KD Kunc : ENNReal} (hCη : 0 ≤ Cη) (hCdη : 0 ≤ Cdη) (hCc : 0 ≤ Cc) (hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B)) (hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B)) (hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖η x‖ ≤ Cη) (hdηbound : ∀ (j : Fin 3), ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖dη j x‖ ≤ Cdη) (hc : ∀ (j : Fin 3), ‖c j‖ ≤ Cc) (hUmeas : MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x i) (MeasureTheory.volume.restrict B)) (hDmeas : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (MeasureTheory.volume.restrict B)) (hU : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ KU) (hD : ∀ (j : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ KD) (hunc : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSource η dη u Du f x i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentred η dη u Du f c x i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc + ENNReal.ofReal Cc * ∑ _j : Fin 3, (ENNReal.ofReal Cη * KD + ENNReal.ofReal Cdη * KU)

Quantitative form of the centred correction estimate.