Pressure Gradient Morrey

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

Pressure Gradient Decay

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

The rate-three exponent bookkeeping for the pressure-gradient decay.

noncomputable def CKN.Core.Step4.pressureGradientSourceExponent (κ : ℝ) : ℝ

Morrey exponent of the pressure-gradient source produced from exponent κ.

Equations

• CKN.Core.Step4.pressureGradientSourceExponent κ = 5 - 6 / κ

theorem CKN.Core.Step4.pressureGradientSourceExponent_eq {κ : ℝ} : pressureGradientSourceExponent κ = 5 - 6 / κ

theorem CKN.Core.Step4.pressureGradientSourceExponent_nonneg {κ : ℝ} (hκ : 6 / 5 ≤ κ) : 0 ≤ pressureGradientSourceExponent κ

theorem CKN.Core.Step4.pressureGradientSourceExponent_lt_three {κ : ℝ} (hκ : 0 < κ) (hκ3 : κ < 3) : pressureGradientSourceExponent κ < 3

theorem CKN.Core.Step4.pressureGradientSourceExponent_routeA : pressureGradientSourceExponent (25 / 11) = 59 / 25

theorem CKN.Core.Step4.pressureGradientSourceExponent_endgame : pressureGradientSourceExponent (25 / 9) = 71 / 25

theorem CKN.Core.Step4.pressureGradientRateThree_admissible : 0 ≤ pressureGradientSourceExponent (25 / 11) ∧ pressureGradientSourceExponent (25 / 11) < 3 ∧ 0 ≤ pressureGradientSourceExponent (25 / 9) ∧ pressureGradientSourceExponent (25 / 9) < 3

The scalar estimate used after the spatial harmonic estimate has been integrated in time. The source term is intentionally left abstract here; the solution-level theorem supplies it from the one-scale estimate.

theorem CKN.Core.Step4.pressure_gradient_two_scale_decay_from_components {Φ V : ℝ → ℝ} {C₃ ρ r : ℝ} (hC₃ : 0 ≤ C₃) (hρ : 0 < ρ) (hr : 0 < r) (hrr : r ≤ ρ / 8) (hΦ : 0 ≤ Φ ρ) (hdecomp : Φ r ≤ V r + Φ (r / 2)) (hpart : V r ≤ C₃ * (r / ρ) ^ 3 * V ρ) (hharm : Φ (r / 2) ≤ C₃ * (r / ρ) ^ 3 * (Φ ρ + V ρ)) : Φ r ≤ 2 * C₃ * (r / ρ) ^ 3 * (Φ ρ + V ρ)

A geometric-scale form of the standard decay iteration. This is the exact discrete form used by the Morrey wrapper.

theorem CKN.Core.Step4.pressure_gradient_geometric_decay {θ σ A B : ℝ} {a : ℕ → ℝ} (hθ : 0 ≤ θ) (hσ : 0 ≤ σ) (hθσ : θ < σ) (hA : 0 ≤ A) (hB : 0 ≤ B) (ha : 0 ≤ a 0) (haA : a 0 ≤ A) (hrec : ∀ (n : ℕ), a (n + 1) ≤ θ * a n + B * σ ^ n) (n : ℕ) : a n ≤ (A + B / (σ - θ)) * σ ^ n

The exponent forced by the convection source and the force.

theorem CKN.Core.Step4.routeA_morreyNorm_add_le {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => f z + g z) ≤ Foundation.Parabolic.Morrey.morreyNorm 3 25 f + Foundation.Parabolic.Morrey.morreyNorm 3 25 g

theorem CKN.Core.Step4.routeA_morreyNorm_const_mul_finite {c : ℝ} (hc : 0 < c) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hN : Foundation.Parabolic.Morrey.morreyNorm 3 25 f < ⊤) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => c * f z) < ⊤

theorem CKN.Core.Step4.routeA_morreyNorm_mono_ae {p q : ℝ} (hp : 0 ≤ p) {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hfg : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), |f z| ≤ |g z|) : Foundation.Parabolic.Morrey.morreyNorm p q f ≤ Foundation.Parabolic.Morrey.morreyNorm p q g