The centred source correction meets the first slot at the two instances

The correction splits into the divergence source, the cutoff-derivative quadratic terms and the mean-gradient terms. The first carries the established affine budget; the second is measured by a Hölder product of the velocity against the mean-free velocity, whose own budget is the gradient one through the L⁶ Sobolev–Poincaré display; the third pairs the gradient against the slice mean. The actual Riesz fields of the three sources then satisfy the clipped-cell estimate above an explicit threshold depending on nothing.

noncomputable def CKN.Core.Step4.originASlotM2Coefficient : ENNReal

The absolute coefficient of the centred correction relative to the divergence-source budget.

Equations

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

noncomputable def CKN.Core.Step4.originASlotM2Threshold (_q : ℝ) : ℝ

The Calderón–Zygmund threshold above which the centred correction meets the affine first-slot budget.

Equations

• CKN.Core.Step4.originASlotM2Threshold _q = (CKN.Core.Step4.pressureRieszMorreyConstant (25 / 9) * CKN.Core.Step4.originASlotM2Coefficient).toReal

theorem CKN.Core.Step4.originASlotM2Coefficient_lt_top : originASlotM2Coefficient < ⊤

theorem CKN.Core.Step4.originASlot_M2_correction_mass_instances (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal) : 5 / 2 < q → 25 / 3 ≤ τ → τ ≤ 25 → 0 ≤ C_CZ → originASlotM2Threshold q ≤ C_CZ → ∀ (hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32), 0 < R₁ → R₁ < R₀ → R₀ < 3 / 4 → 0 ≤ ε → 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 ε → ∀ (i : Fin 3), ∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (r : ℝ), 0 < r → r ≤ 1 / 256 → have hρ := ⋯; have η := mollifiedBallCutoff z.1 hρ; have c := sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u; ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η (spatialDeriv η) (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) j) x) (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)))