Backward Gaussian test functions

The backward test function used in the local energy calculation is recorded together with its nonnegativity.

noncomputable def CKN.Foundation.Heat.backwardHeatTestFunction (r : ℝ) (x : Parabolic.Vec3) (t : ℝ) : ℝ

Rescaled backward heat test function centered at time r ^ 2.

Equations

• CKN.Foundation.Heat.backwardHeatTestFunction r x t = r ^ 2 * CKN.Foundation.Heat.heatKernel x (r ^ 2 - t)

theorem CKN.Foundation.Heat.backwardHeatTestFunction_nonneg {r : ℝ} {x : Parabolic.Vec3} {t : ℝ} : 0 < r → t < r ^ 2 → 0 ≤ backwardHeatTestFunction r x t