The force potentials of a slice carry a weak gradient, with no condition on div f

The last two summands p₇ + p₈ of the local pressure decomposition eq:pk are the force potentials. The class def:sws imposes no condition on the spatial divergence of the force, so display (3.5) of the pressure-gradient section must carry them: they do not cancel in general.

The first, p₇ = -∑ⱼ ∂ⱼN * (η fⱼ), is a coordinate sum of Newtonian derivative potentials of the cut-off force, which is exactly the shape the Calderón–Zygmund selection differentiates, with the L^{6/5} bound of that selection. The second, p₈ = -∑ⱼ N * (∂ⱼη fⱼ), has its density carried by the cutoff annulus, hence is C¹ on the inner ball B_{ρ/2}(x₀) with the far-field gradient bound of eq:har-Ck at order one; its classical gradient there is its weak gradient. Adding the two produces one slice field, in L^{6/5} of the inner ball with the ρ^{-1/2} weight of display (3.5).

theorem CKN.Core.Step4.hasWeakPartialDerivOn_neg {B : Set Foundation.Parabolic.Vec3} {k : Fin 3} {w g : Foundation.Parabolic.Vec3 → ℝ} (h : HasWeakPartialDerivOn B k w g) : HasWeakPartialDerivOn B k (fun (x : Vec 3) => -w x) fun (x : Vec 3) => -g x

A weak partial derivative changes sign with its function.

theorem CKN.Core.Step4.slice_force_weak_gradient_of_slice_data (C_CZ M : ℝ) (hC_CZ : 0 ≤ C_CZ) (hM : 0 ≤ M) {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hP1 : ∀ (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hmem : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => mollifiedBallCutoff x₀ hρ y * f (y, s) j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hcs : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mollifiedBallCutoff x₀ hρ y * f (y, s) j) (hp8 : ContDiffOn ℝ (↑1) (pressureP8 (mollifiedBallCutoff x₀ hρ) f s) (euclideanBall x₀ (ρ / 2))) (hsup : ∀ x ∈ euclideanBall x₀ (ρ / 2), Foundation.Parabolic.vec3EuclideanNorm (classicalGradient (pressureP8 (mollifiedBallCutoff x₀ hρ) f s) x) ≤ M * (ρ ^ 3)⁻¹) : ∃ (g : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), ∀ (k : Fin 3), HasWeakPartialDerivOn (euclideanBall x₀ (ρ / 2)) k (pressureP7 (mollifiedBallCutoff x₀ hρ) f s + pressureP8 (mollifiedBallCutoff x₀ hρ) f s) (g k) ∧ MeasureTheory.LocallyIntegrableOn (g k) (euclideanBall x₀ (ρ / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (g k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))) ≤ ENNReal.ofReal (C_CZ * ∑ j : Fin 3, MeasureTheory.lpNorm (fun (y : Foundation.Parabolic.Vec3) => mollifiedBallCutoff x₀ hρ y * f (y, s) j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + M * ρ ^ (-1 / 2))

The force slot of display (3.5) on one slice, from the data of the two force densities. The Calderón–Zygmund selection hP1 differentiates the first force potential; the second is differentiated classically on the inner ball, where it is C¹ with the gradient bound M ρ^{-3}. The resulting field is the coordinate weak gradient of p₇ + p₈ there, and its L^{6/5} norm carries the ρ^{-1/2} weight of the display.

noncomputable def CKN.Core.Step4.sliceForceGradientConstant : ℝ

The constant of the force slot of display (3.5): the order-one far-field constant of eq:har-Ck for the annular Newtonian potential, against the gradient size of the ball cutoff of lem:cutoff.

Equations

• CKN.Core.Step4.sliceForceGradientConstant = 400 * CKN.Core.Step4.sliceForcePotentialConstant * CKN.cutoffGradientConstant

theorem CKN.Core.Step4.sliceForceGradientConstant_nonneg : 0 ≤ sliceForceGradientConstant

The constant of the force slot of display (3.5) is nonnegative.

noncomputable def CKN.Core.Step4.sliceForceGradientBound (C_CZ C₈ : ℝ) (x₀ : Foundation.Parabolic.Vec3) {ρ : ℝ} (hρ : 0 < ρ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : ℝ

The L^{6/5} size of the force slot of display (3.5) on one time slice: the Calderón–Zygmund norm of the cut-off force together with the ρ^{-1/2}-weighted L¹ norm of the force on the ball.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.slice_force_weak_gradient_of_slice_sources (C_CZ C₈ : ℝ) (hC_CZ : 0 ≤ C_CZ) (hC₈ : sliceForceGradientConstant ≤ C₈) {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hP1 : ∀ (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hmem : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => mollifiedBallCutoff x₀ hρ y * f (y, s) j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hint : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv (mollifiedBallCutoff x₀ hρ) j y * f (y, s) j) MeasureTheory.volume) (hbnd : ∀ (j : Fin 3), ∫ (y : Foundation.Parabolic.Vec3), ‖spatialDeriv (mollifiedBallCutoff x₀ hρ) j y * f (y, s) j‖ ≤ cutoffGradientConstant / ρ * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (f (y, s))) : ∃ (g : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), ∀ (k : Fin 3), HasWeakPartialDerivOn (euclideanBall x₀ (ρ / 2)) k (pressureP7 (mollifiedBallCutoff x₀ hρ) f s + pressureP8 (mollifiedBallCutoff x₀ hρ) f s) (g k) ∧ MeasureTheory.LocallyIntegrableOn (g k) (euclideanBall x₀ (ρ / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (g k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall x₀ (ρ / 2))) ≤ ENNReal.ofReal (sliceForceGradientBound C_CZ C₈ x₀ hρ f s)

The force slot of display (3.5) on one slice, from the L^{6/5} membership of the first force density and the L¹ data of the second. The two force potentials of eq:pk have a common coordinate weak gradient on the inner ball B_{ρ/2}(x₀), with the L^{6/5} bound of the display.

theorem CKN.Core.Step4.exists_slice_field_of_ae {B : Set Foundation.Parabolic.Vec3} {J : Set ℝ} {w : ℝ → Foundation.Parabolic.Vec3 → ℝ} {Sw : ℝ → ℝ} (h : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (g : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), ∀ (k : Fin 3), HasWeakPartialDerivOn B k (w s) (g k) ∧ MeasureTheory.LocallyIntegrableOn (g k) B MeasureTheory.volume ∧ MeasureTheory.eLpNorm (g k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ ENNReal.ofReal (Sw s)) : ∃ (gw : ℝ → Fin 3 → Foundation.Parabolic.Vec3 → ℝ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (k : Fin 3), HasWeakPartialDerivOn B k (w s) (gw s k) ∧ MeasureTheory.LocallyIntegrableOn (gw s k) B MeasureTheory.volume ∧ MeasureTheory.eLpNorm (gw s k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ ENNReal.ofReal (Sw s)

A slice field selected for almost every time becomes a single function of time. This is the measurable-free Skolemization that display (3.5) needs before the space-time selection of the pressure gradient is applied.

theorem CKN.Core.Step4.exists_slice_force_weak_gradient_ae_of_sws (C_CZ C₈ : ℝ) (hC_CZ : 0 ≤ C_CZ) (hC₈ : sliceForceGradientConstant ≤ C₈) {Ω : 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) (hP1 : ∀ (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) : ∃ (gw : ℝ → Fin 3 → Foundation.Parabolic.Vec3 → ℝ), ∀ᵐ (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) (gw s k) ∧ MeasureTheory.LocallyIntegrableOn (gw s k) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm (gw s k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal (sliceForceGradientBound C_CZ C₈ z.1 hρ f s)

The force slot of display (3.5) for a suitable weak solution, with no condition on the divergence of the force. For almost every time of the one-sided interval J_ρ the two force potentials of eq:pk have a common coordinate weak gradient on the inner ball B_{ρ/2}(x₀), locally integrable there and bounded in L^{6/5} by the Calderón–Zygmund norm of the cut-off force together with the ρ^{-1/2}-weighted L¹ norm of the force on B_ρ(x₀).