Pressure Gradient Origin Budget Sufficient #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Sufficient origin-carrier budget conditions #
The first result transports an explicit inflated whole-carrier budget to the margin-scale one-sided constant. The second is the independent scalar bound on the exponent appearing in that inflation factor.
theorem
CKN.Core.Step4.margin_clause_of_inflated_budget
{q τ C_CZ R₀ R₁ ε : ℝ}
{KU KD A B : ENNReal}
(hR₁ : 0 < R₁)
(hR₁34 : R₁ < 3 / 4)
(hA : A ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε))
(hB :
B * ENNReal.ofReal ((R₁ / ((1 - R₁) / 4)) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))) ≤ ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1))
:
Endgame.oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((1 - R₁) / 4) A B ≤ oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD
The two displayed budget inequalities suffice to bound the one-sided Morrey constant measured at the origin-carrier margin scale by the specialized pressure-gradient constant.
theorem
CKN.Core.Step4.growth_exponent_range
{q τ : ℝ}
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτ' : τ ≤ 25)
:
Under the admissible ranges for q and τ, the exponent in the
origin-carrier budget inflation lies between 59 / 25 and 71 / 25.