Slice Selected Gradient Centred Source Tensor Def

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

The force-free centred pressure source

The first pressure potential is paired with the singly centred tensor pressureUTensor u c. Its divergence source contains neither the force term nor the centring correction. The force remains in the separate p₇ + p₈ pressure contribution.

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

Force-free centred divergence-form source paired with η · pressureUTensor.

Equations

• CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor η dη u Du 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))

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

Source-Morrey alias for pressureDivergenceCutoffSourceCentredTensor.

Equations

• CKN.Core.Step4.sourceMorreyCutoffVCentredTensor η dη u Du c = CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor η dη u Du c

def CKN.Core.Step4.sourceMorreyCutoffVCentredTensorSpacetime (η : Foundation.Parabolic.Vec3 → ℝ) (dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3

Spacetime force-free source with a time-dependent spatial mean.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.sourceMorreyCutoffVCentredTensor_hasCompactSupport {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} {c : Foundation.Parabolic.Vec3} (hηsupport : tsupport η ⊆ B) (hdηsupport : ∀ (j : Fin 3), tsupport (dη j) ⊆ B) (hBcompact : IsCompact B) (i : Fin 3) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentredTensor η dη u Du c x i

Each source component has compact support wherever the cutoff and its derivatives are supported.

theorem CKN.Core.Step4.sourceMorreyCutoffVCentredTensor_add_force {η : 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 x : Foundation.Parabolic.Vec3} {i : Fin 3} : sourceMorreyCutoffVCentredTensor η dη u Du c x i = sourceMorreyCutoffVCentred η dη u Du f c x i + η x * f x i

The force-free centred source is the old force-bearing centred source plus the force contribution η f.

theorem CKN.Core.Step4.sourceMorreyCutoffVCentredTensor_slice_bound_le_full_add_force {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} {p : ENNReal} (hp : 1 ≤ p) : MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentredTensor η dη u Du c x i) p (MeasureTheory.volume.restrict B) ≤ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentred η dη u Du f c x i) p (MeasureTheory.volume.restrict B) + MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => η x * f x i) p (MeasureTheory.volume.restrict B)

On every L^p endpoint with p ≥ 1, its slice norm is bounded by the norm of the full centred source plus the norm of η f.