Morrey improvement from actual localized sources

The potential comparison uses almost-everywhere finiteness. Measurability of the potential and finiteness of the explicit Adams constants are derived, rather than supplied as extra inputs.

theorem CKN.Core.Endgame.bootstrap_morrey_of_sources {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 (w : Foundation.Parabolic.ParabolicPoint) => g w i) MeasureTheory.volume) (hh : ∀ (j i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => h j w i) MeasureTheory.volume) (hgN : (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w)) < ⊤) (hhN : ∀ (j : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w)) < ⊤) (hgsupp : ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, g w = 0) (hhsupp : ∀ (j : Fin 3), ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, h j w = 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)) < ⊤

The first velocity-exponent improvement follows from the real localized source norms and representation, without all-point integrability assumptions.