Local L^{3/2} membership and linear growth of the force potentials p₇ and p₈

The two force terms of the local pressure decomposition eq:pk, estimated in lem:pk-bounds, are

• p₇ = ∑ⱼ (∂ⱼN) * (η fⱼ), a sum of first-derivative Newtonian potentials, and
• p₈ = -∑ⱼ N * ((∂ⱼη) fⱼ), a sum of Newtonian potentials,

where N = -newtonianKernel. In Lean, pressureNewtonianDerivativePotential is convolution with -∂ⱼN, so the outer minus in pressureP7 gives the positive sign above. The data use the cutoff η and force f of a suitable weak solution. The cancellation argument for the force feeds p₇ + p₈ into the Liouville step of ext:newtonian, which needs p₇ + p₈ to be L^{3/2} on every round ball euclideanBall 0 ρ with local norm at most C * (1 + ρ).

This file assembles exactly that pair of statements from the single-potential estimates of CKN.Foundation.Euclidean.PotentialLocalLpGrowth, with the constant an explicit finite sum of the single-potential constants. The hypotheses are per-slice: at a fixed time s, each of the six data functions (∂ⱼη) fⱼ(·, s) and η fⱼ(·, s) is of class L^q with 6/5 ≤ q and vanishes off a closed ball. The exponent range 6/5 ≤ q contains the pressure exponent 3/2 and the force exponents q > 5/2 of def:sws.

Negated finite sums of potentials

theorem CKN.Foundation.Euclidean.neg_sum_memLp_and_lpNorm_growth {F : Fin 3 → Parabolic.Vec3 → ℝ} {C : Fin 3 → ℝ} (hmem : ∀ (j : Fin 3) (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (F j) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hb : ∀ (j : Fin 3) (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (F j) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C j * (1 + ρ)) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (fun (x : Parabolic.Vec3) => -∑ j : Fin 3, F j x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (fun (x : Parabolic.Vec3) => -∑ j : Fin 3, F j x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (∑ j : Fin 3, C j) * (1 + ρ)

A negated finite sum of functions that are L^{3/2} on every round ball with linear growth is again of that class, with the sum of the constants.

The explicit growth constants of p₇ and p₈

noncomputable def CKN.Foundation.Euclidean.pressureP8GrowthConstant (η : Parabolic.Vec3 → ℝ) (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (s R : ℝ) : ℝ

The linear-growth constant of p₈ at time s, for data supported in the closed ball of radius R: the sum over the three components of the Newtonian-potential constants.

Equations

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

noncomputable def CKN.Foundation.Euclidean.pressureP7GrowthConstant (η : Parabolic.Vec3 → ℝ) (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (s R : ℝ) : ℝ

The linear-growth constant of p₇ at time s, for data supported in the closed ball of radius R: the sum over the three components of the derivative-potential constants.

Equations

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

theorem CKN.Foundation.Euclidean.pressureP8GrowthConstant_nonneg (η : Parabolic.Vec3 → ℝ) (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (s R : ℝ) : 0 ≤ pressureP8GrowthConstant η f s R

theorem CKN.Foundation.Euclidean.pressureP7GrowthConstant_nonneg (η : Parabolic.Vec3 → ℝ) (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (s : ℝ) {R : ℝ} (hR : 0 < R) : 0 ≤ pressureP7GrowthConstant η f s R

The force potentials on every round ball

theorem CKN.Foundation.Euclidean.pressureP8_memLp_and_lpNorm_growth {η : Parabolic.Vec3 → ℝ} {f : Parabolic.ParabolicPoint → Parabolic.Vec3} {s R q : ℝ} (hR : 0 < R) (hq : 6 / 5 ≤ q) (hdata : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) (ENNReal.ofReal q) MeasureTheory.volume) (hsupp : ∀ (j : Fin 3), ∀ y ∉ Metric.closedBall 0 R, spatialDeriv η j y * f (y, s) j = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ pressureP8GrowthConstant η f s R * (1 + ρ)

p₈ is L^{3/2} on every round ball about the origin, with local norm at most pressureP8GrowthConstant η f s R * (1 + ρ).

theorem CKN.Foundation.Euclidean.pressureP7_memLp_and_lpNorm_growth {η : Parabolic.Vec3 → ℝ} {f : Parabolic.ParabolicPoint → Parabolic.Vec3} {s R q : ℝ} (hR : 0 < R) (hq : 6 / 5 ≤ q) (hdata : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Parabolic.Vec3) => η y * f (y, s) j) (ENNReal.ofReal q) MeasureTheory.volume) (hsupp : ∀ (j : Fin 3), ∀ y ∉ Metric.closedBall 0 R, η y * f (y, s) j = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureP7 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureP7 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ pressureP7GrowthConstant η f s R * (1 + ρ)

p₇ is L^{3/2} on every round ball about the origin, with local norm at most pressureP7GrowthConstant η f s R * (1 + ρ).

The pair of hypotheses consumed by the force cancellation argument

theorem CKN.Foundation.Euclidean.pressureP7_add_pressureP8_memLp_and_lpNorm_growth {η : Parabolic.Vec3 → ℝ} {f : Parabolic.ParabolicPoint → Parabolic.Vec3} {s R q : ℝ} (hR : 0 < R) (hq : 6 / 5 ≤ q) (hdata₇ : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Parabolic.Vec3) => η y * f (y, s) j) (ENNReal.ofReal q) MeasureTheory.volume) (hsupp₇ : ∀ (j : Fin 3), ∀ y ∉ Metric.closedBall 0 R, η y * f (y, s) j = 0) (hdata₈ : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) (ENNReal.ofReal q) MeasureTheory.volume) (hsupp₈ : ∀ (j : Fin 3), ∀ y ∉ Metric.closedBall 0 R, spatialDeriv η j y * f (y, s) j = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureP7 η f s + pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureP7 η f s + pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (pressureP7GrowthConstant η f s R + pressureP8GrowthConstant η f s R) * (1 + ρ)

The local L^{3/2} membership and the linear growth of p₇ + p₈ on the round balls: this is the exact pair of hypotheses that the force cancellation of lem:pk-bounds feeds to the Liouville step of ext:newtonian.

theorem CKN.Foundation.Euclidean.pressureP7_add_pressureP8_growthConstant_nonneg (η : Parabolic.Vec3 → ℝ) (f : Parabolic.ParabolicPoint → Parabolic.Vec3) (s : ℝ) {R : ℝ} (hR : 0 < R) : 0 ≤ pressureP7GrowthConstant η f s R + pressureP8GrowthConstant η f s R

The growth constant of p₇ + p₈ is nonnegative, which is the remaining component of the force cancellation hypothesis.