Morrey Form Uniform

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

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

Uniform small-scale velocity coefficient derived from the Gagliardo interpolation bound.

Equations

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

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

Uniform small-scale gradient coefficient derived from the energy decay bound.

Equations

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

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

Uniform small-scale pressure coefficient derived from pressure decay.

Equations

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

noncomputable def CKN.uniformVelocityReferenceIntegral (M r₂ : ℝ) : ENNReal

Velocity integral bound on the reference cylinder of radius r₂ / 2.

Equations

• CKN.uniformVelocityReferenceIntegral M r₂ = ENNReal.ofReal ((r₂ / 2) ^ 2 * (2 * CKN.gagliardoConstant * (M * (r₂ / 2) ^ (2 / 5))) ^ 3)

noncomputable def CKN.uniformGradientReferenceIntegral (M r₂ : ℝ) : ENNReal

Gradient integral bound on the reference cylinder of radius r₂ / 2.

Equations

• CKN.uniformGradientReferenceIntegral M r₂ = ENNReal.ofReal (M ^ 2 * (r₂ / 2) ^ (9 / 5))

noncomputable def CKN.uniformPressureReferenceIntegral (M r₂ : ℝ) : ENNReal

Pressure integral bound on the reference cylinder of radius r₂ / 2.

Equations

• CKN.uniformPressureReferenceIntegral M r₂ = ENNReal.ofReal (M ^ (3 / 2) * (r₂ / 2) ^ (13 / 5))

noncomputable def CKN.uniformVelocityLargeConstant (M r₂ : ℝ) : ENNReal

Velocity Morrey coefficient combining the small-scale estimate and reference-cylinder bound.

Equations

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

noncomputable def CKN.uniformGradientLargeConstant (M r₂ : ℝ) : ENNReal

Gradient Morrey coefficient combining the small-scale estimate and reference-cylinder bound.

Equations

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

noncomputable def CKN.uniformPressureLargeConstant (M r₂ : ℝ) : ENNReal

Pressure Morrey coefficient combining the small-scale estimate and reference-cylinder bound.

Equations

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

theorem CKN.step2_morrey_form_uniform (M r₂ : ℝ) (hM : 1 ≤ M) (hr₂ : 0 < r₂) : ∃ (Kᵤ : ENNReal) (K_Du : ENNReal) (Kₚ : ENNReal), Kᵤ < ⊤ ∧ K_Du < ⊤ ∧ Kₚ < ⊤ ∧ ∀ {Ω : 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}, IsSuitableWeakSolutionIntegrable Ω I q u Du p f → ∀ (z₀ : Foundation.Parabolic.ParabolicPoint), Metric.ball z₀ (2 * r₂) ⊆ spaceTimeSet Ω I → (∀ 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)) → (∀ (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ₚ

Step 2 with constants chosen before the solution data. The constants are functions only of the decay constant and the reference radius.

theorem CKN.step2_morrey_form_uniform_membership {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), Foundation.Parabolic.Morrey.morreyBallNorm 3 (25 / 3) (Q₂.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ Kᵤ) (hDu : ∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyBallNorm 2 (25 / 8) (Q₂.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ K_Du) (hp : Foundation.Parabolic.Morrey.morreyBallNorm (3 / 2) (25 / 8) (Q₂.indicator p) ≤ 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) < ⊤

Membership is the finite-constant corollary of the uniform norm export.

theorem CKN.step2_morrey_form_uniform_fixed_scale {Ω : 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} {z : Foundation.Parabolic.ParabolicPoint} {r₂ M : ℝ} (hr₂ : 0 < r₂) (hM : 1 ≤ M) (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 (2 * r₂)) ⊆ spaceTimeSet Ω I) (hdec : max (max (alpha u z r₂) (beta u Du z r₂)) (delta p z r₂ ^ 2) ≤ M * r₂ ^ (2 / 5)) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≤ ENNReal.ofReal (r₂ ^ 2 * (2 * gagliardoConstant * (M * r₂ ^ (2 / 5))) ^ 3) ∧ ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal (spatialGradientSq u Du w) ≤ ENNReal.ofReal (M ^ 2 * r₂ ^ (9 / 5)) ∧ ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r₂, ENNReal.ofReal |p w| ^ (3 / 2) ≤ ENNReal.ofReal (M ^ (3 / 2) * r₂ ^ (13 / 5))

Fixed-scale Step 2 bounds with the scale and constants before the solution data. These are the localized estimates used to make the large Morrey scales depend only on the decay constant and the reference radius.