Spatial slice data for the centred source #
The regularity and incompressibility clauses of def:sws supply the local
norms, weak gradients, and zero trace used in eq:pressure-gradient-decomposition.
The exceptional set is chosen before quantifying over spatial test functions.
theorem
CKN.Core.Step4.centredSWS_slice_data
{Ω : 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)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) 3
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ∧ MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du (x, s)) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ∧ MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, s)) (ENNReal.ofReal q)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ∧ ∀ (i : Fin 3),
HasWeakGradientOn (Foundation.Parabolic.vec3Ball z.1 ρ) (fun (x : Vec 3) => u (x, s) i) fun (x : Vec 3) =>
Du (x, s) i
The spatial regularity data of def:sws on almost every cylinder slice.
theorem
CKN.Core.Step4.centredSWS_trace_zero_ae
{Ω : 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)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (fun (x : Foundation.Parabolic.Vec3) =>
∑ i : Fin 3, Du (x, s) i i) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)]
0
Incompressibility in def:sws gives a zero spatial gradient trace on one
common almost-everywhere time set.
theorem
CKN.Core.Step4.centredSWS_pairing_ae
{Ω : 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), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
∑ i : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) u Du c (x, s) 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 centred force-free source supplies the pairing in
eq:pressure-gradient-decomposition on almost every suitable-solution slice.