Space Second Deriv

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

theorem CKN.Foundation.Heat.heatKernelSpaceDerivative_fderiv_apply_basisVec {x : Parabolic.Vec3} {t : ℝ} (ht : 0 < t) (i : Fin 3) : (fderiv ℝ (fun (z : Parabolic.Vec3) => heatKernelSpaceDerivative z t i) x) (basisVec i) = heatKernelSpaceSecondDerivative x t i

The spatial derivative of the heat kernel's first derivative in direction i equals the second spatial derivative of the heat kernel in direction i.