A measurable-norm envelope for the harmonic force term

Fixed-radius Young and far-field bounds control the force contribution of eq:pressure-gradient-morrey by spatial source norms on its cutoff ball.

Force-potential growth constants controlled by source norms

The force constant in the harmonic part of eq:pressure-gradient-morrey contains a local potential norm and a far-field mass. Both are bounded by the spatial L^{6/5} norm of the compactly supported source, with explicit fixed-radius coefficients. These estimates assert no shrinking-cell power.

theorem CKN.Core.Step4.origin_newtonian_growth_constant_bound {G : Foundation.Parabolic.Vec3 → ℝ} {R : ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : ENNReal.ofReal (Foundation.Euclidean.newtonianPotentialGrowthConstant G R) ≤ MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume * (MeasureTheory.eLpNorm (Foundation.Euclidean.truncatedNewtonianPotentialKernel (R + 2 * R)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (2 * (4 * Real.pi)⁻¹ * invNormBallConstant ^ (2 / 3)) * MeasureTheory.volume (Metric.closedBall 0 R) ^ (1 / 6))

The Newtonian potential's growth constant is bounded by the source norm and a fixed-radius kernel and volume coefficient.

theorem CKN.Core.Step4.origin_newtonian_derivative_growth_constant_bound {G : Foundation.Parabolic.Vec3 → ℝ} {R : ℝ} (i : Fin 3) (hR : 0 < R) (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : ENNReal.ofReal (Foundation.Euclidean.newtonianDerivativePotentialGrowthConstant i G R) ≤ MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume * (MeasureTheory.eLpNorm (Foundation.Euclidean.truncatedNewtonianDerivative (R + 2 * R) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (4 * (4 * Real.pi)⁻¹ / (2 * R) * invNormBallConstant ^ (2 / 3)) * MeasureTheory.volume (Metric.closedBall 0 R) ^ (1 / 6))

The derivative-potential growth constant is controlled by the same source norm, retaining its explicit inverse-radius far-field coefficient.

noncomputable def CKN.Core.Step4.originNewtonianCoefficient (R : ℝ) : ENNReal

Fixed-radius coefficient for the Newtonian potential.

Equations

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

noncomputable def CKN.Core.Step4.originNewtonianDerivativeCoefficient (R : ℝ) (i : Fin 3) : ENNReal

Fixed-radius coefficient for the derivative Newtonian potential.

Equations

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

noncomputable def CKN.Core.Step4.originForceGrowthEnvelope (R : ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : ENNReal

The force-growth envelope uses only spatial norms on the origin ball.

Equations

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

theorem CKN.Core.Step4.origin_harmonic_force_le_envelope {R : ℝ} (hR : 0 < R) {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (s : ℝ) (hf : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R))) : ENNReal.ofReal (harmonicRemainderForceBound (0, 0) hR f s) ≤ originForceGrowthEnvelope R f s

The harmonic force-growth constant is bounded by its norm envelope whenever the three force components belong to the local source space.