Backward Potential Identity

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

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