Derivatives #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.caccioppoli_heat_spatialPartial
{x₀ : Foundation.Parabolic.Vec3}
{t₀ r : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(ht : z.2 - t₀ < r ^ 2)
(i : Fin 3)
:
spatialPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatTestFunction r (w.1 - x₀) (w.2 - t₀))
i z = r ^ 2 * Foundation.Heat.heatKernelSpaceDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i
theorem
CKN.caccioppoli_heat_timePartial
{x₀ : Foundation.Parabolic.Vec3}
{t₀ r : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(ht : z.2 - t₀ < r ^ 2)
:
timePartial
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatTestFunction r (w.1 - x₀) (w.2 - t₀))
z = -r ^ 2 * Foundation.Heat.heatKernelTimeDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀))
theorem
CKN.caccioppoli_heat_secondSpatialPartial
{x₀ : Foundation.Parabolic.Vec3}
{t₀ r : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(ht : z.2 - t₀ < r ^ 2)
(i : Fin 3)
:
spatialSecondPartial
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Heat.backwardHeatTestFunction r (w.1 - x₀) (w.2 - t₀))
i i z = r ^ 2 * Foundation.Heat.heatKernelSpaceSecondDerivative (z.1 - x₀) (r ^ 2 - (z.2 - t₀)) i