Morrey cell estimates for the first velocity-improvement round

The first round of the velocity improvement of prop:bootstrap starts from u ∈ M^{3,25/3} and must place the heat-slot source in M^{6/5,25/11} and the derivative-slot source in M^{3,25/6}. Both slots are produced from a bounded multiplier applied to a field whose Morrey norm is known on a metric ball, so the estimates below are stated for abstract exponents: a lowering step for the pair of exponents, and the local integrability that a finite Morrey norm supplies.

theorem CKN.Core.Step4.morreyNorm_lt_top_of_lower_exponents {P P₀ θ θ₀ : ℝ} {B : Set Foundation.Parabolic.ParabolicPoint} {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hP : 1 ≤ P) (hPP₀ : P ≤ P₀) (hP₀θ₀ : P₀ ≤ θ₀) (hPθ : P ≤ θ) (hθθ₀ : θ ≤ θ₀) (hR : 0 < R) (hB : B ⊆ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R) (hAE : AEMeasurable g MeasureTheory.volume) (hzero : ∀ w ∉ B, g w = 0) (hN : Foundation.Parabolic.Morrey.morreyNorm P₀ θ₀ g < ⊤) : Foundation.Parabolic.Morrey.morreyNorm P θ g < ⊤

Lowering both Morrey exponents of a field supported in a parabolic cylinder keeps the seminorm finite: the integrability exponent drops from P₀ to P on the bounded cells, and the Morrey exponent drops from θ₀ to θ because the field vanishes outside the cylinder.

theorem CKN.Core.Step4.integrableOn_ball_of_morreyBallNorm {P τ r : ℝ} {z : Foundation.Parabolic.ParabolicPoint} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hP : 1 ≤ P) (hPτ : P ≤ τ) (hr : 0 < r) (hf : AEMeasurable f (MeasureTheory.volume.restrict (Metric.ball z r))) (hN : Foundation.Parabolic.Morrey.morreyBallNorm P τ ((Metric.ball z r).indicator f) < ⊤) : MeasureTheory.IntegrableOn f (Metric.ball z r) MeasureTheory.volume

A field with finite metric-ball Morrey seminorm on a parabolic ball is integrable there: the integrability exponent may be lowered to one, and the resulting Morrey bound controls the integral over the ball.