The force potentials of a slice carry a vanishing weak gradient

The last two summands p₇ + p₈ of the local pressure decomposition eq:pk are the force potentials. When the force is distributionally divergence free in space-time the two cancel on almost every slice, and the slice field of display (3.5) needs no contribution from them: the zero function is their weak gradient on the inner ball, with vanishing L^{6/5} norm.

The cancellation itself is the whole-space harmonic uniqueness statement of the force section; this file only converts it into the weak-gradient shape that display (3.5) consumes.

theorem CKN.Core.Step4.hasWeakPartialDerivOn_zero_of_ae_eq_zero {B : Set Foundation.Parabolic.Vec3} {w : Foundation.Parabolic.Vec3 → ℝ} (k : Fin 3) (hw : w =ᵐ[MeasureTheory.volume] 0) : HasWeakPartialDerivOn B k w fun (x : Vec 3) => 0

A function vanishing almost everywhere has the zero function as each of its weak partial derivatives on every set.

theorem CKN.Core.Step4.locallyIntegrableOn_zero (B : Set Foundation.Parabolic.Vec3) : MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => 0) B MeasureTheory.volume

The zero function is locally integrable on every set.

theorem CKN.Core.Step4.slice_force_weak_gradient_ae_of_ae_zero {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hzero : ∀ᵐ (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) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (k : Fin 3), (HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) fun (x : Vec 3) => 0) ∧ MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => 0) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => 0) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal 0

Display (3.5) for the force potentials of a slice, in the case where they cancel: the zero field is their weak gradient on the inner ball and its L^{6/5} norm is zero.

theorem CKN.Core.Step4.slice_force_weak_gradient_ae_of_sws_divergence_free {Ω : 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) (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => f (x, s) i) MeasureTheory.volume) (hdiv : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (k : Fin 3), (HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) fun (x : Vec 3) => 0) ∧ MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => 0) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => 0) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal 0

The force slot of display (3.5) for a suitable weak solution whose force is distributionally divergence free in space-time: the slice force potentials cancel and their weak gradient on the inner ball is zero.