Quantitative Morrey improvement for symmetric source carriers

A symmetric parabolic ball lies in a backward cylinder whose top time is shifted forward. The quantitative potential estimate is independent of this enlargement, so its numerical coefficient is unchanged.

theorem CKN.Core.Endgame.bootstrap_morrey_le_of_component_sources_on_ball (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 ∉ Metric.ball z₀ R, g z = 0) (hhsupp : ∀ (j : Fin 3), ∀ z ∉ Metric.ball z₀ 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)

Component sources supported in a symmetric metric ball yield the same numerical Morrey improvement as sources in a backward cylinder.