Numerical bounds for the first Morrey improvement

The constants in Adams' estimate and in lowering the integrability exponent are retained. This gives a bound determined by the source bounds, not by a new existential constant chosen after the solution.

noncomputable def CKN.Core.Endgame.bootstrapOrderTwoCoefficient : ENNReal

The order-two Adams coefficient after lowering integrability to three.

Equations

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

noncomputable def CKN.Core.Endgame.bootstrapOrderOneCoefficient : ENNReal

The order-one Adams coefficient after lowering integrability to three.

Equations

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

noncomputable def CKN.Core.Endgame.bootstrapSourceMorreyBound (KF KG : ENNReal) : ENNReal

The numerical velocity bound determined by the two source bounds.

Equations

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

theorem CKN.Core.Endgame.bootstrapSourceMorreyBound_lt_top {KF KG : ENNReal} (hKF : KF < ⊤) (hKG : KG < ⊤) : bootstrapSourceMorreyBound KF KG < ⊤

Both coefficients and hence the resulting bound are finite.

theorem CKN.Core.Endgame.potential_majorant_morrey_le (KF KG : ENNReal) {g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume) (hh : ∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) MeasureTheory.volume) (hNF : (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g z)) ≤ KF) (hNG : ∀ (j : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j z)) ≤ KG) : Foundation.Parabolic.Morrey.morreyNorm 3 25 (Step4.pointwisePotentialMajorant g h) ≤ bootstrapSourceMorreyBound KF KG

The potential majorant retains an explicit bound from the source bounds.

theorem CKN.Core.Endgame.bootstrap_morrey_le_of_sources (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume) (hh : ∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) MeasureTheory.volume) (hNF : (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g z)) ≤ KF) (hNG : ∀ (j : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j z)) ≤ KG) (hgsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, g z = 0) (hhsupp : ∀ (j : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, h j z = 0) (hrep : v =ᵐ[MeasureTheory.volume] Step3.duhamelPotential g h) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (v z)) ≤ bootstrapSourceMorreyBound KF KG

The first Morrey improvement has a source-uniform numerical bound. Actual kernel finiteness is derived before applying the real majorant.

theorem CKN.Core.Endgame.bootstrap_morrey_le_of_component_sources (KF KG : ENNReal) (hKF : KF < ⊤) (hKG : KG < ⊤) {v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume) (hh : ∀ (j i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) MeasureTheory.volume) (hNF : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) ≤ KF) (hNG : ∀ (j i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (z : Foundation.Parabolic.ParabolicPoint) => h j z i) ≤ KG) (hgsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, g z = 0) (hhsupp : ∀ (j : Fin 3), ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, h j z = 0) (hrep : v =ᵐ[MeasureTheory.volume] Step3.duhamelPotential g h) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (v z)) ≤ bootstrapSourceMorreyBound (3 * KF) (3 * KG)

Componentwise source bounds supply the numerical bootstrap bound with the explicit three-coordinate aggregation factor.