Route AGradient Producer Uniform Morrey

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

Lowering the second Morrey exponent on a parabolic ball

The vector Morrey membership of def:parabolic-morrey is defined on a metric ball of finite radius. A function whose Morrey seminorm is finite at an exponent pair (P, τ) also has finite seminorm at any pair (P, τ') with τ' ≤ τ, because the ball sits inside a fixed parabolic cylinder and the bounded-support Morrey inclusion is available there. The results here expose that monotonicity directly on the metric-ball formulation, which is the shape consumed downstream.

theorem CKN.Core.Step4.morreyVecMem_ball_of_exponent_le {P τ τ' : ℝ} (hP : 1 ≤ P) (hPτ' : P ≤ τ') (hτ'τ : τ' ≤ τ) {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hu : morreyVecMem P τ (Metric.ball z₀ R) u) : morreyVecMem P τ' (Metric.ball z₀ R) u

Parabolic Morrey inclusion on a ball of finite radius: if a vector field has finite Morrey seminorm for the exponent pair (P, τ) on Metric.ball z₀ R, then it has finite seminorm for (P, τ') whenever P ≤ τ' ≤ τ. This is the ball-level form of def:parabolic-morrey, obtained from the bounded-support inclusion for the cylinder containing the ball.

theorem CKN.Core.Step4.morreyVecMem_ball_three_base_of_le {τ : ℝ} (hτ : 25 / 3 ≤ τ) {z₀ : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hu : morreyVecMem 3 τ (Metric.ball z₀ R) u) : morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u

Parabolic Morrey inclusion on a ball of finite radius at the base exponent P = 3: a vector field with finite Morrey seminorm for (3, τ) on Metric.ball z₀ R has finite seminorm for (3, 25 / 3) whenever 25 / 3 ≤ τ. This is def:parabolic-morrey at the exponent used by the gradient producer.