Pressure Gradient One Sided KP

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

Enlarged one-sided pressure-gradient majorant

This file preserves oneSidedPressureGradientKP and introduces a larger majorant with an additive 6/5-power term in its small-cell budget and the clipped-scale inflation in its whole-carrier budget.

Main results

• oneSidedPressureGradientKP_le_oneSidedPressureGradientKP': the old majorant is bounded by the enlarged one without parameter assumptions.
• clipped_clause_le_oneSidedPressureGradientKP': the original raw budget certificates imply the clipped-scale conclusion throughout 0 < R₁ < 3/4.
• oneSidedPressureGradientQuantitative_to_KP': transports the explicit AE binder with the old majorant to the binder with the enlarged majorant.

The adapter direction is from the AE producer stated with KP to the larger KP' bound; a closer consuming the enlarged binder should use this direction.

noncomputable def CKN.Core.Step4.oneSidedPressureGradientKP' (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : ENNReal

The enlarged pressure-gradient majorant. Its A budget adds the raised 6/5 power to the old A budget, and its B budget absorbs the clipped-scale inflation, floored at one.

Equations

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

theorem CKN.Core.Step4.oneSidedPressureGradientKP'_lt_top (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (hKU : KU < ⊤) (hKD : KD < ⊤) : oneSidedPressureGradientKP' q τ C_CZ R₀ R₁ ε KU KD < ⊤

The enlarged majorant is finite for finite velocity and gradient budgets and an admissible force exponent.

theorem CKN.Core.Step4.oneSidedPressureGradientKP_le_oneSidedPressureGradientKP' (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD ≤ oneSidedPressureGradientKP' q τ C_CZ R₀ R₁ ε KU KD

The original one-sided pressure-gradient majorant is pointwise bounded by the enlarged majorant.

theorem CKN.Core.Step4.clipped_clause_le_oneSidedPressureGradientKP' {q τ C_CZ R₀ R₁ ε : ℝ} {KU KD A B : ENNReal} (hR₁ : 0 < R₁) (hR₁' : R₁ < 3 / 4) (hA : A ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε)) (hB : B ≤ ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1)) : Endgame.oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((1 - R₁) / 2) A B ≤ oneSidedPressureGradientKP' q τ C_CZ R₀ R₁ ε KU KD

Raw A and B budget certificates imply the clipped-scale estimate against the enlarged majorant for every 0 < R₁ < 3/4; the clipped-scale inflation is absorbed into its B slot.

theorem CKN.Core.Step4.oneSidedPressureGradientQuantitative_to_KP' (hGA : oneSidedPressureGradientQuantitative) (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → KU < ⊤ → KD < ⊤ → oneSidedPressureGradientKP' q τ C_CZ R₀ R₁ ε KU KD < ⊤ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {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 → closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I → (∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) → (∀ (i j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8) ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) → ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε → ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Ω I U J → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ oneSidedPressureGradientKP' q τ C_CZ R₀ R₁ ε KU KD

Convert the explicit AE binder with the original majorant to the same quantitative binder with the enlarged majorant. This is the direction needed when the closer consumes KP': each old output estimate is transported upward using oneSidedPressureGradientKP_le_oneSidedPressureGradientKP'.