Force Divergence Free Bridge #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.pressure_force_slice_divergenceFree_of_spacetime
{I : Set ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hloc :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => f (x, s) i) MeasureTheory.volume)
(hslice :
∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, DistributionalDivergenceFree fun (x : Foundation.Parabolic.Vec3) => f (x, s)
The space-time distributional force identity implies the slice-wise distributional divergence condition used by the force cancellation consumers.
theorem
CKN.pressure_force_eq_zero_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)
(hdiv :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), DistributionalDivergenceFree fun (x : Foundation.Parabolic.Vec3) => f (x, s))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s =ᵐ[MeasureTheory.volume] 0
The force cancellation theorem with the slice-wise divergence interface used by the pressure consumers.