Backward Potential Kernel Bridge

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

theorem CKN.Foundation.Heat.heatConv_spatial_kernel_transfer {u : Parabolic.Vec3 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huSupport : HasCompactSupport u) {t : ℝ} (ht : 0 < t) (i : Fin 3) (x : Parabolic.Vec3) : heatConv t (fun (y : Parabolic.Vec3) => (fderiv ℝ u y) (basisVec i)) x = ∫ (y : Parabolic.Vec3), heatKernelSpaceDerivative y t i * u (x - y)

theorem CKN.Foundation.Heat.backwardTestPotential_spatialPartial_eq_backwardHeatPotentialSpatial {ζ : Parabolic.Vec3 × ℝ → ℝ} (hζ : ContDiff ℝ (↑⊤) ζ) (hζc : HasCompactSupport ζ) (i : Fin 3) (x : Parabolic.Vec3) (t : ℝ) : spatialPartial (have this := fun (z : Parabolic.ParabolicPoint) => backwardTestPotential ζ z; this) i (x, t) = backwardHeatPotentialSpatial i (have this := ζ; this) (x, t)