Uniform force-source Morrey bounds

A scalar source supported on the unit cylinder and dominated there by the force inherits its global integral bound. The global Lebesgue-to-Morrey estimate and unit-support exponent reduction preserve a fully numerical bound, with no conversion of infinite integrals to real numbers.

noncomputable def CKN.Core.Endgame.forceSourceMorreyBound (q ε₀ : ℝ) : ENNReal

The force-source bound determined by the unit-cylinder data size.

Equations

• CKN.Core.Endgame.forceSourceMorreyBound q ε₀ = MeasureTheory.volume (CKN.Foundation.Parabolic.parabolicCylinder 0 0 1) ^ (5 / 6 - 1 / q) * ENNReal.ofReal ε₀ ^ (1 / q)

theorem CKN.Core.Endgame.forceSourceMorreyBound_lt_top (q ε₀ : ℝ) (hq : 5 / 2 < q) : forceSourceMorreyBound q ε₀ < ⊤

The numerical force-source bound is finite in the admissible force range.

theorem CKN.Core.Endgame.force_source_integral_le_of_small_data (q ε₀ : ℝ) (hq : 0 < q) {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p F : Foundation.Parabolic.ParabolicPoint → ℝ} (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (hdom : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 1), |F z| ≤ Foundation.Parabolic.vec3EuclideanNorm (f z)) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, F z = 0) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint), ENNReal.ofReal |F z| ^ q ≤ ENNReal.ofReal ε₀

The original small-data sum controls the global force-source integral when the source vanishes outside the unit cylinder and is dominated inside.

theorem CKN.Core.Endgame.force_source_morrey_le_of_small_data (q ε₀ : ℝ) (hq : 5 / 2 < q) {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (hdom : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 1), |F z| ≤ Foundation.Parabolic.vec3EuclideanNorm (f z)) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, F z = 0) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) q F ≤ forceSourceMorreyBound q ε₀

The force-source Morrey estimate at the original force exponent.

theorem CKN.Core.Endgame.force_source_paper_morrey_le_of_small_data (q ε₀ : ℝ) (hq : 5 / 2 < q) {u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p F : Foundation.Parabolic.ParabolicPoint → ℝ} (hF : AEMeasurable F MeasureTheory.volume) (hsmall : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀) (hdom : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 1), |F z| ≤ Foundation.Parabolic.vec3EuclideanNorm (f z)) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1, F z = 0) : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) F ≤ forceSourceMorreyBound q ε₀

On unit support, the paper heat-source exponent is reached without increasing the numerical bound.