The inner-ball gradient of the second force potential p₈

The local pressure decomposition eq:pk writes the pressure on a ball as p₁ + (p₂ + … + p₆) + (p₇ + p₈). The last summand

pressureP8 η f s = fun x => -∑ j, pressureNewtonianPotential (fun y => spatialDeriv η j y * f (y, s) j) x

is the second force potential. With η = mollifiedBallCutoff x₀ hρ its density spatialDeriv η j · * f (·, s) j is carried by the cutoff annulus pressureAnnulus x₀ ρ = B(x₀, 3ρ/4) \ B(x₀, 13ρ/20), so on the inner ball B(x₀, ρ/2) the Newtonian kernel is smooth in the evaluation point and the potential is C¹, with the far-field gradient bound of eq:har-Ck and the separation 3ρ/20 of lem:cutoff. Display (3.5) of the pressure-gradient section consumes exactly that: the classical gradient of p₈ on the inner ball, measured in the Euclidean norm, is controlled by the L¹ size of the annular density with a constant that is uniform in the ball and its centre.

noncomputable def CKN.Core.Step4.sliceForcePotentialConstant : ℝ

The uniform constant of the inner-ball gradient bound for the annular Newtonian potential, read off from the all-order kernel estimate of eq:har-Ck at order one. It depends on no parameter of the ball geometry.

Equations

• CKN.Core.Step4.sliceForcePotentialConstant = CKN.Core.Step4.sliceForcePotentialConstant._proof_4.choose

theorem CKN.Core.Step4.sliceForcePotentialConstant_nonneg : 0 ≤ sliceForcePotentialConstant

The constant of the inner-ball gradient bound is nonnegative.

theorem CKN.Core.Step4.norm_fderiv_pressureNewtonianPotential_annulus_le {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ pressureAnnulus x₀ ρ, g y = 0) {x : Foundation.Parabolic.Vec3} (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) : ‖fderiv ℝ (pressureNewtonianPotential g) x‖ ≤ sliceForcePotentialConstant * ((3 * ρ / 20) ^ 2)⁻¹ * ∫ (y : Foundation.Parabolic.Vec3), ‖g y‖

The first derivative of the annular Newtonian potential on the inner ball is controlled by the L¹ size of the density times the inverse square of the separation 3ρ/20 of lem:cutoff: this is eq:har-Ck at order one, in the shape display (3.5) of the pressure-gradient section consumes.

theorem CKN.Core.Step4.contDiffOn_pressureP8_halfBall {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hint : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv (mollifiedBallCutoff x₀ hρ) j y * f (y, s) j) MeasureTheory.volume) : ContDiffOn ℝ (↑1) (pressureP8 (mollifiedBallCutoff x₀ hρ) f s) (Foundation.Parabolic.vec3Ball x₀ (ρ / 2))

The second force potential p₈ of the local pressure decomposition eq:pk is C¹ on the inner ball B(x₀, ρ/2) whenever its density is integrable: the density of the cutoff is carried by the annulus pressureAnnulus x₀ ρ, on which the potential is smooth (eq:har-Ck).

theorem CKN.Core.Step4.vec3EuclideanNorm_classicalGradient_pressureP8_le {x₀ : Foundation.Parabolic.Vec3} {ρ A : ℝ} (hρ : 0 < ρ) (hA0 : 0 ≤ A) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hint : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv (mollifiedBallCutoff x₀ hρ) j y * f (y, s) j) MeasureTheory.volume) (hA : ∀ (j : Fin 3), ∫ (y : Foundation.Parabolic.Vec3), ‖spatialDeriv (mollifiedBallCutoff x₀ hρ) j y * f (y, s) j‖ ≤ A) {x : Foundation.Parabolic.Vec3} (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ (ρ / 2)) : Foundation.Parabolic.vec3EuclideanNorm (classicalGradient (pressureP8 (mollifiedBallCutoff x₀ hρ) f s) x) ≤ 400 * sliceForcePotentialConstant * A * (ρ ^ 2)⁻¹

Display (3.5) of the pressure-gradient section for the second force potential: on the inner ball B(x₀, ρ/2) the Euclidean norm of the classical gradient of p₈ is bounded by 400 · c · A · ρ⁻², where A bounds the L¹ sizes of the annular components of the density and c is the uniform constant of eq:har-Ck at order one.