Concrete pressure-gradient identification from suitability #
One fixed spatial localization gives the force-free centred source, a near force source, and the smooth sum of the harmonic and far force potentials. Every locally integrable weak pressure derivative agrees with their signed completed-operator decomposition on almost every slice.
theorem
CKN.Core.Step4.ae_weak_pressure_derivative_eq_fixed_riesz_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)
:
have η := mollifiedBallCutoff z.1 hρ;
have c := sourceSliceCentredMean z.1 ρ u;
have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du c;
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ),
MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) MeasureTheory.volume →
HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) g →
g =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 (ρ / 2))]
fun (x : Foundation.Parabolic.Vec3) =>
-∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator
(Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => V (y, s) j)
x + classicalGradient (harmonicPressurePart η u c p s + pressureP8 η f s) x i + ∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x
Suitability identifies every weak pressure derivative on the half ball with the fixed-localization completed Riesz terms and smooth remainder.