Route AOne Round Final

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

Route AOne Round

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

def CKN.Core.Step4.routeAGradientSlotRepresentation : Prop

Heat-potential representation interface with an explicitly selected weak pressure gradient.

Equations

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

def CKN.Core.Step4.routeAFinalSourcePackage : Prop

Final localized-source integrability and Morrey estimates required by the bootstrap route.

Equations

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

theorem CKN.Core.Step4.routeA_one_round_velocity_improvement_of_producers_final (hG : routeAGradientProducer) (hL : routeAGradientSlotRepresentation) (hS : routeAFinalSourcePackage) (q : ℝ) : 5 / 2 < q → ∀ {Ω : 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 → ∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ), 0 < R → Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I → morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u → (∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) → morreyVecMem 3 25 (Metric.ball z₀ (R / 4)) u