Morrey Form

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

noncomputable def CKN.pressureSmallConstant (M : ℝ) : ENNReal

Pressure coefficient controlling the small-scale Morrey integral bounds.

Equations

• CKN.pressureSmallConstant M = ENNReal.ofReal (M ^ (3 / 2) * 8 ^ (13 / 5))

noncomputable def CKN.gradientSmallConstant (M : ℝ) : ENNReal

Gradient coefficient controlling the small-scale Morrey integral bounds.

Equations

• CKN.gradientSmallConstant M = ENNReal.ofReal (M ^ 2 * 8 ^ (9 / 5))

noncomputable def CKN.velocitySmallConstant (M : ℝ) : ENNReal

Velocity coefficient obtained from Sobolev interpolation in the small-scale Morrey estimate.

Equations

• One or more equations did not get rendered due to their size.

The Step 2 decay certificate is converted into the three Morrey bounds.

theorem CKN.step2_morrey_form {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z₀ : Foundation.Parabolic.ParabolicPoint} {r₂ M : ℝ} (hr₂ : 0 < r₂) (hM : 1 ≤ M) (hcarrier : Metric.ball z₀ (2 * r₂) ⊆ spaceTimeSet Ω I) (hdecay : ∀ z ∈ Metric.ball z₀ r₂, ∀ (r : ℝ), 0 < r → r < r₂ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5)) : ∃ (Kᵤ : ENNReal) (K_Du : ENNReal) (Kₚ : ENNReal), Kᵤ < ⊤ ∧ K_Du < ⊤ ∧ Kₚ < ⊤ ∧ morreyVecMem 3 (25 / 3) (Metric.ball z₀ (r₂ / 4)) u ∧ (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ (r₂ / 4)) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) ∧ Foundation.Parabolic.Morrey.morreyBallNorm (3 / 2) (25 / 8) ((Metric.ball z₀ (r₂ / 4)).indicator p) < ⊤ ∧ (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyBallNorm 3 (25 / 3) ((Metric.ball z₀ (r₂ / 4)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ Kᵤ) ∧ (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyBallNorm 2 (25 / 8) ((Metric.ball z₀ (r₂ / 4)).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ K_Du) ∧ Foundation.Parabolic.Morrey.morreyBallNorm (3 / 2) (25 / 8) ((Metric.ball z₀ (r₂ / 4)).indicator p) ≤ Kₚ