Pointwise Potential

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

theorem CKN.Core.Step4.heatPotentialKernel_abs_le_riesz₂ (z w : Foundation.Parabolic.ParabolicPoint) : |HeatPotential.heatPotentialKernel z w| ≤ 1000 * (Foundation.Parabolic.Morrey.parabolicRieszKernel 2 z w).toReal

theorem CKN.Core.Step4.heatPotentialSpatialKernel_abs_le_riesz₁ (i : Fin 3) (z w : Foundation.Parabolic.ParabolicPoint) : |HeatPotential.heatPotentialSpatialKernel i z w| ≤ 300000 * (Foundation.Parabolic.Morrey.parabolicRieszKernel 1 z w).toReal

noncomputable def CKN.Core.Step4.pointwisePotentialMajorant (g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Foundation.Parabolic.ParabolicPoint → ℝ

Riesz-potential majorant for the localized scalar and divergence heat sources.

Equations

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

theorem CKN.Core.Step4.forceLqDataOnBox {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {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) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : localVecLp (spaceTimeSet Ω' J) q f