The centred tensor source #
The source for the first potential in eq:pressure-gradient-decomposition is the
negative divergence of the cutoff tensor. The force belongs to the seventh
and eighth potentials.
theorem
CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor_const
(η : Foundation.Parabolic.Vec3 → ℝ)
(dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ)
(a : Foundation.Parabolic.Vec3)
:
pressureDivergenceCutoffSourceCentredTensor η dη (fun (x : Foundation.Parabolic.Vec3) => a)
(fun (x : Foundation.Parabolic.Vec3) (x_1 x_2 : Fin 3) => 0) a = 0
The tensor source vanishes for constant velocity centred at that same
constant, as required by eq:pressure-gradient-decomposition.
theorem
CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor_memLp
{B : Set Foundation.Parabolic.Vec3}
[MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict B)]
{η : 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η : MeasureTheory.MemLp η ⊤ (MeasureTheory.volume.restrict B))
(hdη : ∀ (j : Fin 3), MeasureTheory.MemLp (dη j) ⊤ (MeasureTheory.volume.restrict B))
(hu :
∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x j) 3 (MeasureTheory.volume.restrict B))
(hDu :
∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du x i j) 2 (MeasureTheory.volume.restrict B))
(i : Fin 3)
:
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η dη u Du c x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B)
Component membership at the source exponent follows from L² gradients
and L³ velocity on a finite-measure set in eq:pressure-gradient-decomposition.
theorem
CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor_memLp_hasCompactSupport
{B : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3}
{c : Foundation.Parabolic.Vec3}
(hB : IsCompact B)
(hη : ContDiff ℝ (↑⊤) η)
(hηB : tsupport η ⊆ B)
(hu :
∀ (j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x j) 3 (MeasureTheory.volume.restrict B))
(hDu :
∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du x i j) 2 (MeasureTheory.volume.restrict B))
:
(∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSourceCentredTensor η (spatialDeriv η) u Du c x i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume) ∧ ∀ (i : Fin 3),
HasCompactSupport fun (x : Foundation.Parabolic.Vec3) =>
pressureDivergenceCutoffSourceCentredTensor η (spatialDeriv η) u Du c x i
Global L^{6/5} membership and compact support of the tensor source in
eq:pressure-gradient-decomposition, from the local velocity and gradient norms.