Morrey Balls

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.step2_morrey_balls {Q₂ : Set Foundation.Parabolic.ParabolicPoint} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {Kᵤ K_Du Kₚ : ENNReal} (hKᵤ : Kᵤ < ⊤) (hK_Du : K_Du < ⊤) (hKₚ : Kₚ < ⊤) (hᵤ : ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → Foundation.Parabolic.Morrey.morreyBallCell 3 (25 / 3) (Q₂.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => u w i) z r ≤ Kᵤ) (hDu : ∀ (i j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → Foundation.Parabolic.Morrey.morreyBallCell 2 (25 / 8) (Q₂.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => Du w i j) z r ≤ K_Du) (hp : ∀ (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → Foundation.Parabolic.Morrey.morreyBallCell (3 / 2) (25 / 8) (Q₂.indicator p) z r ≤ Kₚ) : morreyVecMem 3 (25 / 3) Q₂ u ∧ (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) Q₂ fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) ∧ Foundation.Parabolic.Morrey.morreyBallNorm (3 / 2) (25 / 8) (Q₂.indicator p) < ⊤

Step 2 Morrey bookkeeping. The three cell estimates are the outputs of the local decay estimate, the radius-shifted interpolation glue, and the global finiteness argument. Once those estimates are supplied, the ball Morrey memberships follow directly, with the paper exponents τ₂ = 25/3 and τ₃ = τp = 25/8.