Local L^{3/2} membership and linear growth for Newtonian potentials

The uniqueness half of the Newtonian representation ext:newtonian of the paper applies Liouville's theorem to a function that is L^{3/2} on every round ball euclideanBall 0 ρ with norm growing at most like 1 + ρ. This file produces exactly that pair of statements for the Newtonian potential N * g and for the first-derivative potential ∂ⱼN * g of data g that is compactly supported and of class L^q.

The near-field half is Young's inequality on a ball (CKN.Foundation.Euclidean.PotentialLocalLp); the far-field half is the pointwise decay |N * g| ≲ ‖g‖_{L¹} ‖x‖⁻¹, |∂ⱼN * g| ≲ ‖g‖_{L¹} ‖x‖⁻² of CKN.Pressure.PotentialDecayFarField. The two are combined by the splitting estimate of CKN.Pressure.PotentialDecay, which is where the factor 1 + ρ comes from: the inverse-distance profile ‖x‖⁻¹ has L^{3/2} norm proportional to ρ on the ball of radius ρ.

All the estimates are stated for exponents q ≥ 6/5, which covers the exponent 3/2 of the pressure and the exponents q > 5/2 of the force datum of def:sws.

The explicit constants

noncomputable def CKN.Foundation.Euclidean.newtonianPotentialDecayConstant (G : Parabolic.Vec3 → ℝ) : ℝ

The far-field decay constant of the Newtonian potential of G: the potential is bounded by this constant times ‖x‖⁻¹ outside the support ball.

Equations

• CKN.Foundation.Euclidean.newtonianPotentialDecayConstant G = 2 * (4 * Real.pi)⁻¹ * ∫ (y : CKN.Foundation.Parabolic.Vec3), |G y|

noncomputable def CKN.Foundation.Euclidean.newtonianDerivativePotentialDecayConstant (G : Parabolic.Vec3 → ℝ) (R : ℝ) : ℝ

The far-field decay constant of the first-derivative Newtonian potential of G on the region 2 * R ≤ ‖x‖, measured against ‖x‖⁻¹.

Equations

• CKN.Foundation.Euclidean.newtonianDerivativePotentialDecayConstant G R = (4 * (4 * Real.pi)⁻¹ * ∫ (y : CKN.Foundation.Parabolic.Vec3), |G y|) / (2 * R)

noncomputable def CKN.Foundation.Euclidean.newtonianPotentialGrowthConstant (G : Parabolic.Vec3 → ℝ) (R : ℝ) : ℝ

The linear-growth constant of the Newtonian potential of data supported in the closed ball of radius R: the local L^{3/2} norm near the origin plus the far-field decay constant times the universal ball constant.

Equations

• CKN.Foundation.Euclidean.newtonianPotentialGrowthConstant G R = CKN.invNormGrowthConstant (CKN.pressureNewtonianPotential G) (CKN.Foundation.Euclidean.newtonianPotentialDecayConstant G) R

noncomputable def CKN.Foundation.Euclidean.newtonianDerivativePotentialGrowthConstant (i : Fin 3) (G : Parabolic.Vec3 → ℝ) (R : ℝ) : ℝ

The linear-growth constant of the first-derivative Newtonian potential of data supported in the closed ball of radius R.

Equations

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

theorem CKN.Foundation.Euclidean.newtonianPotentialDecayConstant_nonneg (G : Parabolic.Vec3 → ℝ) : 0 ≤ newtonianPotentialDecayConstant G

theorem CKN.Foundation.Euclidean.newtonianDerivativePotentialDecayConstant_nonneg {R : ℝ} (hR : 0 < R) (G : Parabolic.Vec3 → ℝ) : 0 ≤ newtonianDerivativePotentialDecayConstant G R

theorem CKN.Foundation.Euclidean.newtonianPotentialGrowthConstant_nonneg (G : Parabolic.Vec3 → ℝ) (R : ℝ) : 0 ≤ newtonianPotentialGrowthConstant G R

theorem CKN.Foundation.Euclidean.newtonianDerivativePotentialGrowthConstant_nonneg (i : Fin 3) {R : ℝ} (hR : 0 < R) (G : Parabolic.Vec3 → ℝ) : 0 ≤ newtonianDerivativePotentialGrowthConstant i G R

The far-field decay in the shape required by the growth estimate

theorem CKN.Foundation.Euclidean.tsupport_subset_closedBall_of_zero_outside {G : Parabolic.Vec3 → ℝ} {R : ℝ} (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : tsupport G ⊆ Metric.closedBall 0 R

Data vanishing off a closed ball has its topological support inside that ball.

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_inv_norm_decay {G : Parabolic.Vec3 → ℝ} {R : ℝ} (hR : 0 < R) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) (x : Parabolic.Vec3) : 2 * R ≤ ‖x‖ → |pressureNewtonianPotential G x| ≤ newtonianPotentialDecayConstant G * ‖x‖⁻¹

Inverse-distance decay of the Newtonian potential of compactly supported integrable data.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_inv_norm_decay {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R : ℝ} (hR : 0 < R) (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) (x : Parabolic.Vec3) : 2 * R ≤ ‖x‖ → |pressureNewtonianDerivativePotential i G x| ≤ newtonianDerivativePotentialDecayConstant G R * ‖x‖⁻¹

Inverse-distance decay of the first-derivative Newtonian potential of compactly supported integrable data. The kernel decays like ‖x‖⁻², which on the far region 2 * R ≤ ‖x‖ is stronger than the inverse-distance decay used by the growth estimate.

Local membership and linear growth, for measurable data

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_memLp_and_lpNorm_growth {G : Parabolic.Vec3 → ℝ} {R : ℝ} (hR : 0 < R) (hGmeas : Measurable G) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianPotentialGrowthConstant G R * (1 + ρ)

The Newtonian potential of compactly supported L^{6/5} data is L^{3/2} on every round ball about the origin, with L^{3/2} norm at most C * (1 + ρ).

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_memLp_and_lpNorm_growth {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R : ℝ} (hR : 0 < R) (hGmeas : Measurable G) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianDerivativePotentialGrowthConstant i G R * (1 + ρ)

The first-derivative Newtonian potential of compactly supported L^{6/5} data is L^{3/2} on every round ball about the origin, with L^{3/2} norm at most C * (1 + ρ).

Local membership and linear growth, for L^q data with q ≥ 6/5

The force datum of def:sws is only almost everywhere strongly measurable, so the estimates are restated for such data by passing to the measurable representative supported in the same ball; neither the potentials nor the constants change.

theorem CKN.Foundation.Euclidean.newtonianPotentialDecayConstant_congr {G G' : Parabolic.Vec3 → ℝ} (h : G =ᵐ[MeasureTheory.volume] G') : newtonianPotentialDecayConstant G = newtonianPotentialDecayConstant G'

Almost-everywhere equal data has the same Newtonian decay constant.

theorem CKN.Foundation.Euclidean.newtonianDerivativePotentialDecayConstant_congr {G G' : Parabolic.Vec3 → ℝ} (R : ℝ) (h : G =ᵐ[MeasureTheory.volume] G') : newtonianDerivativePotentialDecayConstant G R = newtonianDerivativePotentialDecayConstant G' R

Almost-everywhere equal data has the same derivative-potential decay constant.

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_memLp_and_lpNorm_growth_of_memLp {G : Parabolic.Vec3 → ℝ} {R q : ℝ} (hR : 0 < R) (hq : 6 / 5 ≤ q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianPotentialGrowthConstant G R * (1 + ρ)

The Newtonian potential of compactly supported L^q data with 6/5 ≤ q is L^{3/2} on every round ball about the origin, with L^{3/2} norm at most C * (1 + ρ). This is the pair of hypotheses consumed by the Liouville step of ext:newtonian.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_memLp_and_lpNorm_growth_of_memLp {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R q : ℝ} (hR : 0 < R) (hq : 6 / 5 ≤ q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianDerivativePotentialGrowthConstant i G R * (1 + ρ)

The first-derivative Newtonian potential of compactly supported L^q data with 6/5 ≤ q is L^{3/2} on every round ball about the origin, with L^{3/2} norm at most C * (1 + ρ).

The two exponents used by the pressure decomposition

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_memLp_and_lpNorm_growth_three_halves {G : Parabolic.Vec3 → ℝ} {R : ℝ} (hR : 0 < R) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianPotentialGrowthConstant G R * (1 + ρ)

The q = 3/2 instance, the exponent of the pressure in def:sws.

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_memLp_and_lpNorm_growth_of_five_halves_lt {G : Parabolic.Vec3 → ℝ} {R q : ℝ} (hR : 0 < R) (hq : 5 / 2 < q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianPotential G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianPotentialGrowthConstant G R * (1 + ρ)

The 5/2 < q instance, the exponent range of the force datum in def:sws.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_memLp_and_lpNorm_growth_three_halves {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R : ℝ} (hR : 0 < R) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianDerivativePotentialGrowthConstant i G R * (1 + ρ)

The q = 3/2 instance for the first-derivative potential.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_memLp_and_lpNorm_growth_of_five_halves_lt {G : Parabolic.Vec3 → ℝ} (i : Fin 3) {R q : ℝ} (hR : 0 < R) (hq : 5 / 2 < q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hGzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureNewtonianDerivativePotential i G) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ newtonianDerivativePotentialGrowthConstant i G R * (1 + ρ)

The 5/2 < q instance for the first-derivative potential.