Quantitative time masses of the localized pressure Riesz sources

A uniform endpoint coefficient puts the localized divergence source into the affine cell budget; the source contains both convection and force.

Pressure Gradient Origin KPAffine Source

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

The divergence source meets the enlarged small-cell budget

For a suitable weak solution with velocity budgets KU, KD on Q_{R₀} and data size ε, the 6/5 power of the Morrey norm of the divergence source Du·u - f of the pressure equation is bounded by X^{6/5}, where X = 3·KU·KD + forceSourceMorreyBound q ε (origin_divergence_source_numerical_bounds_of_sws). That coefficient lies below originKPAffineASlot, so the source meets the enlarged budget with no further analytic input. The linear budget c·3X of oneSidedPressureGradientKP does not dominate X^{6/5} once X > 3c, which is the scaling defect the enlarged budget removes.

theorem CKN.Core.Step4.origin_divergence_source_morrey_rpow_le_KPAffine_slot (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hR : 0 < R₁) (hR₁₀ : R₁ ≤ R₀) (hR₀le : R₀ ≤ 1) {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) (hD : ∀ (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) (hsize : ∫⁻ (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 ε) : (Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm ((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator (fun (w : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) => ∑ j : Fin 3, Du w i j * u w j - f w i) z)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD

The source Morrey norm against the enlarged budget. Under the hypotheses of the origin pressure-gradient obligation, the 6/5 power of the Morrey norm of the vector divergence source on Q_{R₁} lies below originKPAffineASlot q C_CZ ε KU KD.

noncomputable def CKN.Core.Step4.rieszSourceThresholdA : ℝ

An absolute threshold paying for the three spatial Riesz components.

Equations

• CKN.Core.Step4.rieszSourceThresholdA = 3 * (CKN.Core.Step4.pressureRieszMorreyConstant (25 / 9)).toReal

theorem CKN.Core.Step4.pressureRieszMorreyConstant_le_endpoint {κ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) : pressureRieszMorreyConstant κ ≤ pressureRieszMorreyConstant (25 / 9)

The Riesz coefficient is uniformly bounded over the admitted exponent range.

theorem CKN.Core.Step4.three_riesz_constants_le_affine_coefficient {κ C_CZ : ℝ} (hκ : 0 < κ) (hκhi : κ ≤ 25 / 9) (hC : rieszSourceThresholdA ≤ C_CZ) : 3 * pressureRieszMorreyConstant κ ≤ ENNReal.ofReal (|C_CZ| + 1)

The fixed threshold absorbs the sum of three component operator constants.

theorem CKN.Core.Step4.riesz_source_sum_clipped_le_affine_slot (q τ C_CZ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hC : rieszSourceThresholdA ≤ C_CZ) (i : Fin 3) {F T : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hF : ∀ (j : Fin 3), AEMeasurable (F j) MeasureTheory.volume) (hFs : ∀ (j : Fin 3), ∀ᵐ (s : ℝ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => F j (y, s)) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) {L : ℝ} (hsupport : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3) (s : ℝ), L < ‖y‖ → F j (y, s) = 0) (hT : ∀ (j : Fin 3), AEMeasurable (T j) MeasureTheory.volume) (hident : ∀ (j : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => F j (y, s)) (hN : ∀ (j : Fin 3), Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (F j) ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε)) (B : Set Foundation.Parabolic.Vec3) (J : Set ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r) : ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ J, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, T j (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ B)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

Three selected Riesz components of sources with the displayed affine budget satisfy every clipped-cell A estimate above the absolute threshold.

theorem CKN.Core.Step4.exists_origin_riesz_source_affine_bound_of_sws (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτhi : τ ≤ 25) (hC : rieszSourceThresholdA ≤ C_CZ) (hR : 0 < R₁) (hR₁₀ : R₁ ≤ R₀) (hR₀le : R₀ ≤ 1) (hKU : KU < ⊤) (hKD : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hU : ∀ (i : Fin 3), Foundation.Parabolic.Morrey.morreyNorm 3 τ ((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) (hD : ∀ (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) (hsize : ∫⁻ (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 ε) : have F := fun (j : Fin 3) => (Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ k : Fin 3, Du w j k * u w k - f w j; ∃ (T : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ), (∀ (j i : Fin 3), Measurable (T j i)) ∧ (∀ (j i : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j i (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => F j (y, s)) ∧ ∀ (i : Fin 3) (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ), 0 < r → ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, T j i (y, s)) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))

Suitable data admit one jointly measurable near-field Riesz derivative whose three-component sum satisfies the affine A slot on every clipped cell. The source is the outer origin-cylinder restriction of Du·u - f.