Kernel

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

The convolution variables are written explicitly so that the causal heat kernel and its spatial derivatives have one common interface.

def CKN.Core.HeatPotential.pointSub (w v : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.ParabolicPoint

Space-time displacement used as the argument of the translation-invariant heat kernel.

Equations

• CKN.Core.HeatPotential.pointSub w v = (w.1 - v.1, w.2 - v.2)

noncomputable def CKN.Core.HeatPotential.heatPotentialKernel (w v : Foundation.Parabolic.ParabolicPoint) : ℝ

Causal heat kernel evaluated at the space-time displacement of two points.

Equations

• CKN.Core.HeatPotential.heatPotentialKernel w v = CKN.Foundation.Heat.heatKernelPlus (CKN.Core.HeatPotential.pointSub w v)

noncomputable def CKN.Core.HeatPotential.heatPotentialSpatialKernel (i : Fin 3) (w v : Foundation.Parabolic.ParabolicPoint) : ℝ

Spatial derivative of the causal heat kernel at a space-time displacement.

Equations

• CKN.Core.HeatPotential.heatPotentialSpatialKernel i w v = CKN.Foundation.Heat.heatKernelSpaceDerivative (w.1 - v.1) (w.2 - v.2) i

noncomputable def CKN.Core.HeatPotential.heatPotential (F : Foundation.Parabolic.ParabolicPoint → ℝ) (G : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (w : Foundation.Parabolic.ParabolicPoint) : ℝ

Heat potential of a scalar source and spatial divergence sources.

Equations

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

theorem CKN.Core.HeatPotential.heatPotentialKernel_abs_le {w v : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hsep : R ≤ Foundation.Heat.rhoTwo (w.1 - v.1) (w.2 - v.2)) : |heatPotentialKernel w v| ≤ 1000 / R ^ 3

theorem CKN.Core.HeatPotential.heatPotentialSpatialKernel_abs_le {i : Fin 3} {w v : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hsep : R ≤ Foundation.Heat.rhoTwo (w.1 - v.1) (w.2 - v.2)) : |heatPotentialSpatialKernel i w v| ≤ 300000 / R ^ 4

theorem CKN.Core.HeatPotential.heatPotentialSpatialTimeKernel_abs_le {i : Fin 3} {w v : Foundation.Parabolic.ParabolicPoint} {R : ℝ} (hR : 0 < R) (hsep : R ≤ Foundation.Heat.rhoTwo (w.1 - v.1) (w.2 - v.2)) : |Foundation.Heat.heatKernelTimeGradientDerivative (w.1 - v.1) (w.2 - v.2) i| ≤ 30000000000 / R ^ 6