The local tensor source of the pressure gradient #
The source and its tested pairing in eq:pressure-gradient-morrey follow
from the velocity's spatial weak gradient and divergence constraint.
theorem
CKN.Core.Step4.origin_tensor_source_data_ae_of_sws
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(c : ℝ → Foundation.Parabolic.Vec3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) x i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume) ∧ (∀ (i : Fin 3),
HasCompactSupport fun (x : Foundation.Parabolic.Vec3) =>
pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) x i) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∑ i : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), pressureDivergenceCutoffSourceCentredTensor (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) x i * spatialDeriv ψ i x = pressureSecondPairing
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u c (x, s) i j)
ψ
The force-free centred tensor source has the integrability, support,
and pairing properties required by eq:pressure-gradient-morrey.